Try only using TC for conversion in cominductive (not great but let's see)

11 files changed, 36 insertions, 28 deletions

diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 9b80cbd803..7b1aa7a07a 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -47,7 +47,7 @@ DECLARE PLUGIN "ltac_plugin"
 
 let with_delayed_uconstr ist c tac =
   let flags = {
-    Pretyping.use_typeclasses = false;
+    Pretyping.use_typeclasses = Pretyping.NoUseTC;
     solve_unification_constraints = true;
     fail_evar = false;
     expand_evars = true;
@@ -345,7 +345,7 @@ open EConstr
 open Vars
 
 let constr_flags () = {
-  Pretyping.use_typeclasses = true;
+  Pretyping.use_typeclasses = Pretyping.UseTC;
   Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
   Pretyping.fail_evar = false;
   Pretyping.expand_evars = true;
@@ -375,22 +375,22 @@ let refine_tac ist simple with_classes c =
 
 TACTIC EXTEND refine
 | [ "refine" uconstr(c) ] ->
-   { refine_tac ist false true c }
+   { refine_tac ist false Pretyping.UseTC c }
 END
 
 TACTIC EXTEND simple_refine
 | [ "simple" "refine" uconstr(c) ] ->
-   { refine_tac ist true true c }
+   { refine_tac ist true Pretyping.UseTC c }
 END
 
 TACTIC EXTEND notcs_refine
 | [ "notypeclasses" "refine" uconstr(c) ] ->
-   { refine_tac ist false false c }
+   { refine_tac ist false Pretyping.NoUseTC c }
 END
 
 TACTIC EXTEND notcs_simple_refine
 | [ "simple" "notypeclasses" "refine" uconstr(c) ] ->
-   { refine_tac ist true false c }
+   { refine_tac ist true Pretyping.NoUseTC c }
 END
 
 (* Solve unification constraints using heuristics or fail if any remain *)
diff --git a/plugins/ltac/g_auto.mlg b/plugins/ltac/g_auto.mlg
index 3c30c881fb..b4527694ae 100644
--- a/plugins/ltac/g_auto.mlg
+++ b/plugins/ltac/g_auto.mlg
@@ -53,7 +53,7 @@ END
 
 let eval_uconstrs ist cs =
   let flags = {
-    Pretyping.use_typeclasses = false;
+    Pretyping.use_typeclasses = Pretyping.NoUseTC;
     solve_unification_constraints = true;
     fail_evar = false;
     expand_evars = true;
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 9e0b9d3254..b0e26e1def 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -546,7 +546,7 @@ let interp_gen kind ist pattern_mode flags env sigma c =
   (evd,c)
 
 let constr_flags () = {
-  use_typeclasses = true;
+  use_typeclasses = UseTC;
   solve_unification_constraints = true;
   fail_evar = true;
   expand_evars = true;
@@ -564,7 +564,7 @@ let interp_constr = interp_constr_gen WithoutTypeConstraint
 let interp_type = interp_constr_gen IsType
 
 let open_constr_use_classes_flags () = {
-  use_typeclasses = true;
+  use_typeclasses = UseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = true;
@@ -573,7 +573,7 @@ let open_constr_use_classes_flags () = {
 }
 
 let open_constr_no_classes_flags () = {
-  use_typeclasses = false;
+  use_typeclasses = NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = true;
@@ -582,7 +582,7 @@ let open_constr_no_classes_flags () = {
 }
 
 let pure_open_constr_flags = {
-  use_typeclasses = false;
+  use_typeclasses = NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = false;
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 01b12474dd..e0b083a70a 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -239,7 +239,7 @@ let interp_refine ist gl rc =
   } in
   let kind = Pretyping.OfType (pf_concl gl) in
   let flags = {
-    Pretyping.use_typeclasses = true;
+    Pretyping.use_typeclasses = Pretyping.UseTC;
     solve_unification_constraints = true;
     fail_evar = false;
     expand_evars = true;
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 52122c09df..015c26531a 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -189,8 +189,10 @@ let interp_sort_info ?loc evd l =
 
 type inference_hook = env -> evar_map -> Evar.t -> (evar_map * constr) option
 
+type use_typeclasses = NoUseTC | UseTCForConv | UseTC
+
 type inference_flags = {
-  use_typeclasses : bool;
+  use_typeclasses : use_typeclasses;
   solve_unification_constraints : bool;
   fail_evar : bool;
   expand_evars : bool;
@@ -312,9 +314,9 @@ let solve_remaining_evars ?hook flags env ?initial sigma =
   let program_mode = flags.program_mode in
   let frozen = frozen_and_pending_holes (initial, sigma) in
   let sigma =
-    if flags.use_typeclasses
-    then apply_typeclasses ~fail_evar:false ~program_mode env sigma frozen
-    else sigma
+    match flags.use_typeclasses with
+    | UseTC -> apply_typeclasses ~program_mode ~fail_evar:false env sigma frozen
+    | NoUseTC | UseTCForConv -> sigma
   in
   let sigma = match hook with
   | None -> sigma
@@ -1287,21 +1289,25 @@ let ise_pretype_gen flags env sigma lvar kind c =
     if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
   in
   let env = GlobEnv.make ~hypnaming env sigma lvar in
+  let use_tc = match flags.use_typeclasses with
+    | NoUseTC -> false
+    | UseTC | UseTCForConv -> true
+  in
   let sigma', c', c'_ty = match kind with
     | WithoutTypeConstraint | UnknownIfTermOrType ->
-      let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses empty_tycon env sigma c in
+      let sigma, j = pretype ~program_mode ~poly use_tc empty_tycon env sigma c in
       sigma, j.uj_val, j.uj_type
     | OfType exptyp ->
-      let sigma, j = pretype ~program_mode ~poly flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+      let sigma, j = pretype ~program_mode ~poly use_tc (mk_tycon exptyp) env sigma c in
       sigma, j.uj_val, j.uj_type
     | IsType ->
-      let sigma, tj = pretype_type ~program_mode ~poly flags.use_typeclasses empty_valcon env sigma c in
+      let sigma, tj = pretype_type ~program_mode ~poly use_tc empty_valcon env sigma c in
       sigma, tj.utj_val, mkSort tj.utj_type
   in
   process_inference_flags flags !!env sigma (sigma',c',c'_ty)
 
 let default_inference_flags fail = {
-  use_typeclasses = true;
+  use_typeclasses = UseTC;
   solve_unification_constraints = true;
   fail_evar = fail;
   expand_evars = true;
@@ -1310,7 +1316,7 @@ let default_inference_flags fail = {
 }
 
 let no_classes_no_fail_inference_flags = {
-  use_typeclasses = false;
+  use_typeclasses = NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = true;
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index abbb745161..3396c5a0e7 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -44,8 +44,10 @@ type typing_constraint =
   | OfType of types (** A term of the expected type *)
   | WithoutTypeConstraint (** A term of unknown expected type *)
 
+type use_typeclasses = NoUseTC | UseTCForConv | UseTC
+
 type inference_flags = {
-  use_typeclasses : bool;
+  use_typeclasses : use_typeclasses;
   solve_unification_constraints : bool;
   fail_evar : bool;
   expand_evars : bool;
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 000b34ed0a..53254e9511 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -50,7 +50,7 @@ let w_refine (evk,evi) (ltac_var,rawc) env sigma =
   let env = Evd.evar_filtered_env env evi in
   let sigma',typed_c =
     let flags = {
-      Pretyping.use_typeclasses = true;
+      Pretyping.use_typeclasses = Pretyping.UseTC;
       Pretyping.solve_unification_constraints = true;
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true;
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 30ca024a2f..c79aca3d3c 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1223,7 +1223,7 @@ let rec intros_move = function
    or a term with bindings *)
 
 let tactic_infer_flags with_evar = {
-  Pretyping.use_typeclasses = true;
+  Pretyping.use_typeclasses = Pretyping.UseTC;
   Pretyping.solve_unification_constraints = true;
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true;
diff --git a/user-contrib/Ltac2/tac2core.ml b/user-contrib/Ltac2/tac2core.ml
index 2ed854c9f7..72df4d75c8 100644
--- a/user-contrib/Ltac2/tac2core.ml
+++ b/user-contrib/Ltac2/tac2core.ml
@@ -20,7 +20,7 @@ open Proofview.Notations
 let constr_flags =
   let open Pretyping in
   {
-    use_typeclasses = true;
+    use_typeclasses = Pretyping.UseTC;
     solve_unification_constraints = true;
     fail_evar = true;
     expand_evars = true;
@@ -31,7 +31,7 @@ let constr_flags =
 let open_constr_no_classes_flags =
   let open Pretyping in
   {
-  use_typeclasses = false;
+  use_typeclasses = Pretyping.NoUseTC;
   solve_unification_constraints = true;
   fail_evar = false;
   expand_evars = true;
diff --git a/user-contrib/Ltac2/tac2tactics.ml b/user-contrib/Ltac2/tac2tactics.ml
index 30ee1a0b4c..9ca38d64df 100644
--- a/user-contrib/Ltac2/tac2tactics.ml
+++ b/user-contrib/Ltac2/tac2tactics.ml
@@ -20,7 +20,7 @@ let return = Proofview.tclUNIT
 let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r ()
 
 let tactic_infer_flags with_evar = {
-  Pretyping.use_typeclasses = true;
+  Pretyping.use_typeclasses = Pretyping.UseTC;
   Pretyping.solve_unification_constraints = true;
   Pretyping.fail_evar = not with_evar;
   Pretyping.expand_evars = true;
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 458714403a..cc9b840bed 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -147,7 +147,7 @@ let interp_cstrs env (sigma, ind_rel) impls params ind arity =
   let interp_cstr sigma ctyp =
     let flags =
       Pretyping.{ all_no_fail_flags with
-                  use_typeclasses = false;
+                  use_typeclasses = UseTCForConv;
                   solve_unification_constraints = false }
     in
     let sigma, (ctyp, cimpl) = interp_type_evars_impls ~flags env sigma ~impls ctyp in