diff options
| author | Pierre-Marie Pédrot | 2015-10-19 22:52:36 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-20 13:04:00 +0200 |
| commit | f5d8d305c34f9bab21436c765aeeb56a65005dfe (patch) | |
| tree | 7271ad90ee24db93003af945bdaea73ef1aa6787 /tactics/equality.ml | |
| parent | a104cd04f3d245bb45e6ff1db8b4ac10c51f4123 (diff) | |
Renaming Goal.enter field into s_enter.
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 740a165f8d..fdc77be2f3 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -347,7 +347,7 @@ let type_of_clause cls gl = match cls with | Some id -> pf_get_hyp_typ id gl let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl = - Proofview.Goal.nf_s_enter { enter = begin fun gl sigma -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> let isatomic = isProd (whd_zeta hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in @@ -1483,7 +1483,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* on for further iterated sigma-tuples *) let cutSubstInConcl l2r eqn = - Proofview.Goal.nf_s_enter { enter = begin fun gl sigma -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl sigma -> let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in |