diff options
| author | Hugo Herbelin | 2020-03-31 23:48:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-03-31 23:48:49 +0200 |
| commit | 04af77a6b138bb139751053d63651f7187ea9952 (patch) | |
| tree | eda57819139540b03cf1e6a5e15ec558954bb484 /user-contrib | |
| parent | e98e8a03cae984a10fddc8acbe8fd781d4608b24 (diff) | |
| parent | fafc731885f84656ec884d40b843aa62a5991025 (diff) | |
Merge PR #11579: Remove ad-hoc treatment of inductive parameters in implicit arguments
Ack-by: SkySkimmer
Ack-by: gares
Reviewed-by: herbelin
Diffstat (limited to 'user-contrib')
| -rw-r--r-- | user-contrib/Ltac2/tac2core.ml | 4 | ||||
| -rw-r--r-- | user-contrib/Ltac2/tac2tactics.ml | 2 |
2 files changed, 3 insertions, 3 deletions
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; |