diff options
| -rw-r--r-- | tactics/equality.ml | 35 |
1 files changed, 21 insertions, 14 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 2edd67ef8..7a8a3a97b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -317,8 +317,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl = Logic.eq or Jmeq just before *) assert false in - let sigma, elim = Evd.fresh_global (Global.env ()) (Tacmach.New.project gl) (ConstRef c) in - sigma, elim, Safe_typing.empty_private_constants + let Sigma (elim, sigma, p) = Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in + Sigma ((elim, Safe_typing.empty_private_constants), sigma, p) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -336,10 +336,10 @@ let find_elim hdcncl lft2rgt dep cls ot gl = | Ind (ind,u) -> let c, eff = find_scheme scheme_name ind in (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *) - let sigma, elim = - Evd.fresh_global (Global.env ()) (Tacmach.New.project gl) (ConstRef c) + let Sigma (elim, sigma, p) = + Sigma.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in - sigma, elim, eff + Sigma ((elim, eff), sigma, p) | _ -> assert false let type_of_clause cls gl = match cls with @@ -352,14 +352,14 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars d let dep_fun = if isatomic then dependent else dependent_no_evar in let type_of_cls = type_of_clause cls gl in let dep = dep_proof_ok && dep_fun c type_of_cls in - let (sigma,elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in + let Sigma ((elim, effs), sigma, p) = find_elim hdcncl lft2rgt dep cls (Some t) gl in let tac = Proofview.tclEFFECTS effs <*> general_elim_clause with_evars frzevars tac cls c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings); elimrename = None} in - Sigma.Unsafe.of_pair (tac, sigma) + Sigma (tac, sigma, p) end } let adjust_rewriting_direction args lft2rgt = @@ -1451,6 +1451,7 @@ let decomp_tuple_term env c t = in decomprec (mkRel 1) c t let subst_tuple_term env sigma dep_pair1 dep_pair2 b = + let sigma = Sigma.to_evar_map sigma in let typ = get_type_of env sigma dep_pair1 in (* We find all possible decompositions *) let decomps1 = decomp_tuple_term env dep_pair1 typ in @@ -1475,7 +1476,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = (* Retype to get universes right *) let sigma, expected_goal_ty = Typing.type_of env sigma expected_goal in let sigma, _ = Typing.type_of env sigma body in - sigma,body,expected_goal + Sigma.Unsafe.of_pair ((body, expected_goal), sigma) (* Like "replace" but decompose dependent equalities *) (* i.e. if equality is "exists t v = exists u w", and goal is "phi(t,u)", *) @@ -1484,10 +1485,12 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b = let cutSubstInConcl l2r eqn = Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in 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 - let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in + let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in let tac = tclTHENFIRST (tclTHENLIST [ @@ -1496,22 +1499,26 @@ let cutSubstInConcl l2r eqn = ]) (change_concl expected) (* Put in normalized form *) in - Sigma.Unsafe.of_pair (tac, sigma) + Sigma (tac, sigma, p) end } let cutSubstInHyp l2r eqn id = - Proofview.Goal.nf_enter { enter = begin fun gl -> + Proofview.Goal.nf_s_enter { s_enter = begin fun gl -> + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in let typ = pf_get_hyp_typ id gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in - let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in - tclTHENFIRST + let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in + let tac = + tclTHENFIRST (tclTHENLIST [ - (Proofview.Unsafe.tclEVARS sigma); (change_in_hyp None (make_change_arg typ) (id,InHypTypeOnly)); (replace_core (onHyp id) l2r eqn) ]) (change_in_hyp None (make_change_arg expected) (id,InHypTypeOnly)) + in + Sigma (tac, sigma, p) end } let try_rewrite tac = |