diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2014-04-01 11:26:08 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:58 +0200 |
commit | 9e377eade7016bd34d35a5b99eec02f080f387cc (patch) | |
tree | 4101ae533cdea17c5bc65db8b0f2b970b97fca41 | |
parent | 1ed00e4f8cded2a2024b66c3f7f4deee6ecd7c83 (diff) |
Fixes after rebase. The use of pf_constr_of_global is problematic in presence of side-effects...
-rw-r--r-- | tactics/equality.ml | 38 |
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] |