diff options
| author | Pierre-Marie Pédrot | 2018-10-29 11:37:10 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-15 09:50:25 +0100 |
| commit | f26974c7844d6a58d22c3a9d52b93c5a94f19214 (patch) | |
| tree | 8e6438a2f7e7c5ec2c3aae4b1724f0978e0bc8df /src | |
| parent | b06ed5af083e66ab33fbb8f77c8cce5e6b6ed2d3 (diff) | |
Fix compilation w.r.t. coq/coq#8779.
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 } |