aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/ltac/extratactics.mlg12
-rw-r--r--plugins/ltac/g_auto.mlg2
-rw-r--r--plugins/ltac/tacinterp.ml8
-rw-r--r--plugins/ssr/ssrcommon.ml2
-rw-r--r--pretyping/pretyping.ml24
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--proofs/evar_refiner.ml2
-rw-r--r--tactics/tactics.ml2
-rw-r--r--user-contrib/Ltac2/tac2core.ml4
-rw-r--r--user-contrib/Ltac2/tac2tactics.ml2
-rw-r--r--vernac/comInductive.ml2
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:56:37 +0000