diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-19 22:52:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-20 13:04:00 +0200 |
| commit | f5d8d305c34f9bab21436c765aeeb56a65005dfe (patch) | |
| tree | 7271ad90ee24db93003af945bdaea73ef1aa6787 /tactics/autorewrite.ml | |
| parent | a104cd04f3d245bb45e6ff1db8b4ac10c51f4123 (diff) | |
Renaming Goal.enter field into s_enter.
Diffstat (limited to 'tactics/autorewrite.ml')
| -rw-r--r-- | tactics/autorewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml index 9892d2954..2ecba176a 100644 --- a/tactics/autorewrite.ml +++ b/tactics/autorewrite.ml @@ -94,7 +94,7 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tac let one_base general_rewrite_maybe_in tac_main bas = let lrul = find_rewrites bas in let try_rewrite dir ctx c tc = - Proofview.Goal.nf_s_enter { enter = begin fun gl sigma -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in let c' = Vars.subst_univs_level_constr subst c in let sigma = Sigma.to_evar_map sigma in |