diff options
Diffstat (limited to 'src')
| -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 = |