diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/leminv.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 4 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 356b43ec14..48997163de 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -250,7 +250,7 @@ let add_inversion_lemma ~poly name env sigma t sort dep inv_op = let add_inversion_lemma_exn ~poly na com comsort bool tac = let env = Global.env () in let sigma = Evd.from_env env in - let sigma, c = Constrintern.interp_type_evars env sigma com in + let sigma, c = Constrintern.interp_type_evars ~program_mode:false env sigma com in let sigma, sort = Evd.fresh_sort_in_family ~rigid:univ_rigid sigma comsort in try add_inversion_lemma ~poly na env sigma c sort bool tac diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 070b2356e5..afa623741a 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1155,7 +1155,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; +} type evars_flag = bool (* true = pose evars false = fail on evars *) type rec_flag = bool (* true = recursive false = not recursive *) |