[build] Workaround bisect bug with implicit arguments.

This is a bit annoying, but not the end of the world.

c.f. aantron/bisect_ppx#319

interp/constrextern.ml

@@ -965,7 +965,7 @@ let rec extern inctx ?impargs scopes vars r =
          | GRef (ref,us) ->
              let subscopes = find_arguments_scope ref in
              let args = fill_arg_scopes args subscopes scopes in
-             let args = extern_args (extern true) vars args in
+             let args = extern_args (extern ?impargs:None true) vars args in
              (* Try a "{|...|}" record notation *)
              (match extern_record ref args with
              | Some l -> CRecord l
@@ -1282,7 +1282,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
                   let c = make_notation loc specific_ntn (l,ll,bl,bll) in
                   let c = insert_entry_coercion coercion (insert_delimiters c key) in
                   let args = fill_arg_scopes args argsscopes allscopes in
-                  let args = extern_args (extern true) vars args in
+                  let args = extern_args (extern ?impargs:None true) vars args in
                   CAst.make ?loc @@ extern_applied_notation nallargs argsimpls c args)
           | SynDefRule kn ->
               let l =
@@ -1292,7 +1292,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules =
               let cf = Nametab.shortest_qualid_of_syndef ?loc vars kn in
               let a = CRef (cf,None) in
               let args = fill_arg_scopes args argsscopes allscopes in
-              let args = extern_args (extern true) vars args in
+              let args = extern_args (extern ?impargs:None true) vars args in
               let c = CAst.make ?loc @@ extern_applied_syntactic_definition nallargs argsimpls (a,cf) l args in
               if isCRef_no_univ c.CAst.v && entry_has_global custom then c
              else match availability_of_entry_coercion custom InConstrEntrySomeLevel with

pretyping/evarconv.ml

@@ -1611,7 +1611,7 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
   | Evar ev1, Evar ev2 when app_empty ->
     (* solve_evar_evar handles the cases ev1 and/or ev2 are frozen *)
       Success (solve_evar_evar ~force:true
-                 (evar_define evar_unify flags ~choose:true)
+                 (evar_define ?imitate_defs:None evar_unify flags ~choose:true)
                  evar_unify flags env evd
                  (position_problem true pbty) ev1 ev2)
   | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 ->

pretyping/evarsolve.ml

@@ -1514,7 +1514,7 @@ let rec invert_definition unify flags choose imitate_defs
             if choose then (mkVar id, p) else raise (NotUniqueInType sols)
       in
       let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
-      let evd = do_projection_effects unify flags (evar_define unify flags ~choose) env ty !evdref p in
+      let evd = do_projection_effects unify flags (evar_define ?imitate_defs:None unify flags ~choose) env ty !evdref p in
       evdref := evd;
       c
     with
@@ -1527,7 +1527,7 @@ let rec invert_definition unify flags choose imitate_defs
           let ty = find_solution_type (evar_filtered_env env evi) sols in
           let ty' = instantiate_evar_array evi ty argsv in
           let (evd,evar,(evk',argsv' as ev')) =
-            materialize_evar (evar_define unify flags ~choose) env !evdref 0 ev ty' in
+            materialize_evar (evar_define ?imitate_defs:None unify flags ~choose) env !evdref 0 ev ty' in
           let ts = expansions_of_var evd aliases t in
           let test c = isEvar evd c || List.exists (is_alias evd c) ts in
           let filter = restrict_upon_filter evd evk test argsv' in
@@ -1579,7 +1579,7 @@ let rec invert_definition unify flags choose imitate_defs
           (* Make the virtual left evar real *)
           let ty = get_type_of env' evd t in
           let (evd,evar'',ev'') =
-             materialize_evar (evar_define unify flags ~choose) env' evd k ev ty in
+             materialize_evar (evar_define ?imitate_defs:None unify flags ~choose) env' evd k ev ty in
           (* materialize_evar may instantiate ev' by another evar; adjust it *)
           let (evk',args' as ev') = normalize_evar evd ev' in
           let evd =
@@ -1624,7 +1624,7 @@ let rec invert_definition unify flags choose imitate_defs
             | [x] -> x
             | _ ->
               let (evd,evar'',ev'') =
-                materialize_evar (evar_define unify flags ~choose) env' !evdref k ev ty in
+                materialize_evar (evar_define ?imitate_defs:None unify flags ~choose) env' !evdref k ev ty in
               evdref := restrict_evar evd (fst ev'') None (UpdateWith candidates);
               evar'')
         | None ->
@@ -1674,7 +1674,7 @@ and evar_define unify flags ?(choose=false) ?(imitate_defs=true) env evd pbty (e
           (test_success unify) flags env evd pbty evk argsv argsv2
       else
         solve_evar_evar ~force:choose
-          (evar_define unify flags) unify flags env evd pbty ev ev2
+          (evar_define ?choose:None ?imitate_defs:None unify flags) unify flags env evd pbty ev ev2
   | _ ->
   try solve_candidates unify flags env evd ev rhs
   with NoCandidates ->

vernac/classes.ml

@@ -260,7 +260,8 @@ let add_class env sigma cl =
 let intern_info {hint_priority;hint_pattern} =
   let env = Global.env() in
   let sigma = Evd.from_env env in
-  let hint_pattern = Option.map (Constrintern.intern_constr_pattern env sigma) hint_pattern in
+  let hint_pattern = Option.map
+      (Constrintern.intern_constr_pattern ?as_type:None ?ltacvars:None env sigma) hint_pattern in
   {hint_priority;hint_pattern}
 
 (** TODO: add subinstances *)

vernac/comHints.ml

@@ -117,7 +117,10 @@ let interp_hints ~poly h =
     | HintsConstants -> HintsConstants
     | HintsReferences lhints -> HintsReferences (List.map fr lhints)
   in
-  let fp = Constrintern.intern_constr_pattern (Global.env ()) in
+  let fp =
+    Constrintern.intern_constr_pattern ?as_type:None ?ltacvars:None
+      (Global.env ())
+  in
   match h with
   | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints)
   | HintsResolveIFF (l2r, lc, n) ->