diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 2 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 1 |
2 files changed, 0 insertions, 3 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 7384652216..ec10c335e9 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -864,7 +864,6 @@ let constr_flags () = { use_typeclasses = true; solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = true; expand_evars = true } @@ -874,7 +873,6 @@ let open_constr_no_classes_flags () = { use_typeclasses = false; solve_unification_constraints = true; - use_hook = Pfedit.solve_by_implicit_tactic (); fail_evar = false; expand_evars = true } diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index 25431af2ea..b06427bc38 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -21,7 +21,6 @@ let thaw r f = Tac2ffi.app_fun1 f Tac2ffi.unit r () let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; - Pretyping.use_hook = None; Pretyping.fail_evar = not with_evar; Pretyping.expand_evars = true } |