Merge pull request #483 from math-comp/fix-monae

Funclass can be dependent

Author: CohenCyril

HB/common/synthesis.elpi

@@ -153,7 +153,7 @@ pred infer-coercion-tgt i:mixins, o:class.
 infer-coercion-tgt (w-params.cons ID Ty F) CoeClass :-
   @pi-parameter ID Ty x\ infer-coercion-tgt (F x) CoeClass.
 infer-coercion-tgt (w-params.nil _ {{ Type }} _) sortclass.
-infer-coercion-tgt (w-params.nil _ {{ _ -> _ }} _) funclass.
+infer-coercion-tgt (w-params.nil _ {{ forall x, _ }} _) funclass. % do not use {{ _ -> _ }} since Funclass can be a dependent function!
 infer-coercion-tgt (w-params.nil _ T _) (grefclass GR) :- coq.term->gref T GR.
 
 pred w-args.check-key i:list term, i:term, i:list (w-args A), o:prop.