diff options
| author | Maxime Dénès | 2019-02-01 20:59:01 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2019-02-01 20:59:01 +0100 |
| commit | 14cb3c26e5b35a4d824838c76a7cf8d8a0fa35e0 (patch) | |
| tree | 5666ecd8c2af0bc4aff8b7e4351f452b6a5d63e9 | |
| parent | e35f5bb879b4697ff17daad1a2f0d76b71b8e2ca (diff) | |
Adapt to https://github.com/coq/coq/pull/9410
| -rw-r--r-- | src/tac2core.ml | 6 | ||||
| -rw-r--r-- | src/tac2tactics.ml | 4 |
2 files changed, 7 insertions, 3 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 8e92e154ac..b5ae446ed5 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -954,7 +954,8 @@ let constr_flags () = use_typeclasses = true; solve_unification_constraints = true; fail_evar = true; - expand_evars = true + expand_evars = true; + program_mode = false; } let open_constr_no_classes_flags () = @@ -963,7 +964,8 @@ let open_constr_no_classes_flags () = use_typeclasses = false; solve_unification_constraints = true; fail_evar = false; - expand_evars = true + expand_evars = true; + program_mode = false; } (** Embed all Ltac2 data into Values *) diff --git a/src/tac2tactics.ml b/src/tac2tactics.ml index b06427bc38..bc92ab43a8 100644 --- a/src/tac2tactics.ml +++ b/src/tac2tactics.ml @@ -22,7 +22,9 @@ let tactic_infer_flags with_evar = { Pretyping.use_typeclasses = true; Pretyping.solve_unification_constraints = true; Pretyping.fail_evar = not with_evar; - Pretyping.expand_evars = true } + Pretyping.expand_evars = true; + Pretyping.program_mode = false; +} (** FIXME: export a better interface in Tactics *) let delayed_of_tactic tac env sigma = |