diff options
| author | Pierre-Marie Pédrot | 2019-03-14 19:00:34 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-05-10 15:03:19 +0200 |
| commit | 2a79abc613bdf19b53685a40c993f964455904fe (patch) | |
| tree | c0fd8ab20f683c3141934d060852dcda0d569f00 /tactics/tactics.ml | |
| parent | aab47903fb2d3e0085b03d5ade94f4ae644cd76c (diff) | |
No more local reduction functions in Reductionops.
This is extracted from #9710, where we need the environment anyway to compute
iota rules on inductive types with let-bindings. The commit is self-contained,
so I think it could go directly in to save me a few rebases.
Furthermore, this is also related to #11707. Assuming we split cbn from the
other reduction machine, this allows to merge the "local" machine with
the general one, since after this PR they will have the same type. One less
reduction machine should make people happy.
Diffstat (limited to 'tactics/tactics.ml')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index e4809332c5..d0a13a8a40 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1319,7 +1319,7 @@ let cut c = let r = Sorts.relevance_of_sort s in let id = next_name_away_with_default "H" Anonymous (Tacmach.New.pf_ids_set_of_hyps gl) in (* Backward compat: normalize [c]. *) - let c = if normalize_cut then local_strong whd_betaiota sigma c else c in + let c = if normalize_cut then strong whd_betaiota env sigma c else c in Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (Refine.refine ~typecheck:false begin fun h -> let (h, f) = Evarutil.new_evar ~principal:true env h (mkArrow c r (Vars.lift 1 concl)) in @@ -1607,7 +1607,7 @@ let make_projection env sigma params cstr sign elim i n c u = noccur_between sigma 1 (n-i-1) t (* to avoid surprising unifications, excludes flexible projection types or lambda which will be instantiated by Meta/Evar *) - && not (isEvar sigma (fst (whd_betaiota_stack sigma t))) + && not (isEvar sigma (fst (whd_betaiota_stack env sigma t))) && (accept_universal_lemma_under_conjunctions () || not (isRel sigma t)) then let t = lift (i+1-n) t in @@ -3025,7 +3025,7 @@ let specialize (c,lbind) ipat = let flags = { (default_unify_flags ()) with resolve_evars = true } in let clause = clenv_unify_meta_types ~flags clause in let sigma = clause.evd in - let (thd,tstack) = whd_nored_stack sigma (clenv_value clause) in + let (thd,tstack) = whd_nored_stack env sigma (clenv_value clause) in (* The completely applied term is (thd tstack), but tstack may contain unsolved metas, so now we must reabstract them args with there name to have |