aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Matthieu Sozeau <mattam@mattam.org>2014-04-01 11:26:08 +0200
committerGravatar Matthieu Sozeau <mattam@mattam.org>2014-05-06 09:58:58 +0200
commit9e377eade7016bd34d35a5b99eec02f080f387cc (patch)
tree4101ae533cdea17c5bc65db8b0f2b970b97fca41
parent1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 (diff)
Fixes after rebase. The use of pf_constr_of_global is problematic in presence of side-effects...
-rw-r--r--tactics/equality.ml38
1 files changed, 20 insertions, 18 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml
index e91c21293..6e4f46c67 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -285,7 +285,8 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
jmeq_same_dom gl ot)) && not dep
|| Flags.version_less_or_equal Flags.V8_2
then
- match kind_of_term hdcncl with
+ let c =
+ match kind_of_term hdcncl with
| Ind (ind_sp,u) ->
let pr1 =
lookup_eliminator ind_sp (elimination_sort_of_clause cls gl)
@@ -300,17 +301,20 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
begin
try
let _ = Global.lookup_constant c1' in
- c1', Declareops.no_seff
+ c1'
with Not_found ->
let rwr_thm = Label.to_string l' in
error ("Cannot find rewrite principle "^rwr_thm^".")
end
- | _ -> destConstRef pr1, Declareops.no_seff
+ | _ -> destConstRef pr1
end
| _ ->
(* cannot occur since we checked that we are in presence of
Logic.eq or Jmeq just before *)
assert false
+ in
+ let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+ sigma, elim, Declareops.no_seff
else
let scheme_name = match dep, lft2rgt, inccl with
(* Non dependent case *)
@@ -327,7 +331,9 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
match kind_of_term hdcncl with
| Ind (ind,u) ->
let c, eff = find_scheme scheme_name ind in
- c , eff
+ (* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
+ let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+ sigma, elim, eff
| _ -> assert false
let type_of_clause cls gl = match cls with
@@ -340,14 +346,11 @@ 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 (elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
- let tac elim =
- general_elim_clause with_evars frzevars tac cls c t l
+ let (sigma,elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
+ Proofview.V82.tclEVARS sigma <*> 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)}
- in
- Proofview.tclEFFECTS effs <*>
- pf_constr_of_global (ConstRef elim) tac
end
let adjust_rewriting_direction args lft2rgt =
@@ -1220,7 +1223,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
(* arbitrarily take t1' as the injector default value *)
let sigma, (injbody,resty) = build_injector !evdref e_env t1' (mkVar e) cpath in
let injfun = mkNamedLambda e t injbody in
- let congr = Evarutil.evd_comb1 (Evd.fresh_global env) evdref eq.congr in
+ let sigma,congr = Evd.fresh_global env sigma eq.congr in
let pf = applist(congr,[t;resty;injfun;t1;t2]) in
let sigma, pf_typ = Typing.e_type_of env sigma pf in
let inj_clause = apply_on_clause (pf,pf_typ) eq_clause in
@@ -1369,11 +1372,11 @@ let swap_equands eqn =
let swapEquandsInConcl =
Proofview.Goal.raw_enter begin fun gl ->
let (lbeq,u,eq_args) = find_eq_data (pf_nf_concl gl) in
- let args = swap_equality_args eq_args @ [Evarutil.mk_new_meta ()] in
+ let args = swap_equality_args eq_args in
pf_constr_of_global lbeq.sym (fun sym_equal ->
Proofview.V82.tactic (fun gls ->
let c = applist (sym_equal, args) in
- let sigma, cty = pf_apply Typing.e_type_of gl c in
+ let sigma, cty = Tacmach.pf_apply Typing.e_type_of gls c in
refine (applist (c,[Evarutil.mk_new_meta()])) {gls with sigma}))
end
@@ -1383,15 +1386,14 @@ let bareRevSubstInConcl (lbeq,u) body (t,e1,e2) =
Proofview.Goal.raw_enter begin fun gl ->
(* find substitution scheme *)
let eq = Universes.constr_of_global_univ (lbeq.eq,u) in
- let eq_elim, effs = find_elim eq (Some false) false None None gl in
+ let sigma, eq_elim, effs = find_elim eq (Some false) false None None gl in
(* build substitution predicate *)
let p = lambda_create (Proofview.Goal.env gl) (t,body) in
- let sigma, pty = pf_apply Typing.e_type_of gl p in
+ let sigma, pty = Typing.e_type_of (Proofview.Goal.env gl) sigma p in
(* apply substitution scheme *)
let args = [t; e1; p; Evarutil.mk_new_meta (); e2; Evarutil.mk_new_meta ()] in
- Proofview.V82.tclEVARS sigma <*>
- (pf_constr_of_global (ConstRef eq_elim) (fun c ->
- Proofview.V82.tactic (refine (applist (c, args)))))
+ Proofview.V82.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*>
+ (Proofview.V82.tactic (refine (applist (eq_elim, args))))
end
(* [subst_tuple_term dep_pair B]