diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 19:14:51 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-10-29 19:22:59 +0100 |
| commit | 250df8586a776eaadc3553b5ceef98d3696fffdb (patch) | |
| tree | 2e86418dead74cc799f2838b43c8f602dc70cad3 /tactics/equality.ml | |
| parent | f02f64a21863ce03f2da4ff04cd003051f96801f (diff) | |
Removing the evar_map argument from 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 56878f112..2edd67ef8 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 { s_enter = begin fun gl sigma -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> 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 { s_enter = begin fun gl sigma -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> 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 |