diff options
| author | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
|---|---|---|
| committer | Matthieu Sozeau | 2019-02-08 10:44:23 +0100 |
| commit | d1d32f552064b9907fc9815b7412b9a9cde4a0dd (patch) | |
| tree | c4a4b20e92547abae487f8bb1115ba34382f0bfd /tactics | |
| parent | 79b6317f738b6d2d7fdaaaad2cef79a092ec8c77 (diff) | |
| parent | 40ed1b7c5e94f418f9b758ffe1a86e4ad7743267 (diff) | |
Merge PR #9410: Make `Program` a regular attribute
Ack-by: SkySkimmer
Reviewed-by: aspiwack
Reviewed-by: ejgallego
Reviewed-by: gares
Reviewed-by: mattam82
Ack-by: maximedenes
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 f41706c35e..db59f7cfc2 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 *) |