switch argument order of get_hypinfo to get around unerasable-optiona…

…l-argument error in OCaml 4.12.0

src/aac_rewrite.ml

@@ -346,7 +346,7 @@ let aac_rewrite_wrap  ?abort ?(l2r=true) ?(show = false) ?(in_left=true) ?strict
       let check_type x =
         Tacmach.New.pf_conv_x goal x rlt.Coq.Relation.carrier
       in
-      let hypinfo = Coq.Rewrite.get_hypinfo env sigma rew ~l2r ?check_type:(Some check_type) in      
+      let hypinfo = Coq.Rewrite.get_hypinfo env sigma ?check_type:(Some check_type) rew ~l2r in
       let sigma,rewinfo = dispatch env sigma in_left concl hypinfo in
       let sigma =
         match extra with

src/coq.ml

@@ -352,7 +352,7 @@ type hypinfo =
       l2r : bool; 			(** rewriting from left to right  *)
     }
 
-let get_hypinfo env sigma c ?check_type ~l2r  : hypinfo =
+let get_hypinfo env sigma ?check_type c ~l2r : hypinfo =
   let ctype = Typing.unsafe_type_of env sigma c in
   let (rel_context, body_type) = decompose_prod_assum sigma ctype in
   let rec check f e =

src/coq.mli

@@ -174,11 +174,11 @@ type hypinfo =
       l2r : bool; 			(** rewriting from left to right  *)
     }
 
-(** [get_hypinfo H ?check_type l2r] analyse the hypothesis H, and
+(** [get_hypinfo ?check_type H l2r] analyse the hypothesis H, and
     build the related hypinfo. Moreover, an optionnal
     function can be provided to check the type of every free
     variable of the body of the hypothesis.  *)
-val get_hypinfo : Environ.env -> Evd.evar_map ->  EConstr.constr -> ?check_type:(EConstr.types -> bool) -> l2r:bool -> hypinfo
+val get_hypinfo : Environ.env -> Evd.evar_map -> ?check_type:(EConstr.types -> bool) -> EConstr.constr -> l2r:bool -> hypinfo
 
 (** {2 Rewriting with bindings}