diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 49 |
1 files changed, 28 insertions, 21 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index b991defe7..f5ab039b4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -283,12 +283,12 @@ let find_elim hdcncl lft2rgt dep cls ot gl = begin try let _ = Global.lookup_constant c1' in - mkConst c1' + mkConst c1', gl with Not_found -> let rwr_thm = Label.to_string l' in error ("Cannot find rewrite principle "^rwr_thm^".") end - | _ -> pr1 + | _ -> pr1, gl end | _ -> (* cannot occur since we checked that we are in presence of @@ -308,7 +308,10 @@ let find_elim hdcncl lft2rgt dep cls ot gl = | true, _, false -> rew_r2l_forward_dep_scheme_kind in match kind_of_term hdcncl with - | Ind ind -> mkConst (find_scheme scheme_name ind) + | Ind ind -> + let c, eff = find_scheme scheme_name ind in + let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in + mkConst c, gl | _ -> assert false let type_of_clause gl = function @@ -319,7 +322,7 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac sigma c t l with_evars frze let isatomic = isProd (whd_zeta hdcncl) in let dep_fun = if isatomic then dependent else dependent_no_evar in let dep = dep_proof_ok && dep_fun c (type_of_clause gl cls) in - let elim = find_elim hdcncl lft2rgt dep cls (Some t) gl in + let elim, gl = find_elim hdcncl lft2rgt dep cls (Some t) gl in general_elim_clause with_evars frzevars tac cls sigma c t l (match lft2rgt with None -> false | Some b -> b) {elimindex = None; elimbody = (elim,NoBindings)} gl @@ -775,14 +778,16 @@ let ind_scheme_of_eq lbeq = let kind = if kind == InProp then Elimschemes.ind_scheme_kind_from_prop else Elimschemes.ind_scheme_kind_from_type in - mkConst (find_scheme kind (destInd lbeq.eq)) + let c, eff = find_scheme kind (destInd lbeq.eq) in + mkConst c, eff let discrimination_pf e (t,t1,t2) discriminator lbeq = - let i = build_coq_I () in - let absurd_term = build_coq_False () in - let eq_elim = ind_scheme_of_eq lbeq in - (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) + let i = build_coq_I () in + let absurd_term = build_coq_False () in + let eq_elim, eff = ind_scheme_of_eq lbeq in + (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term), + eff let eq_baseid = Id.of_string "e" @@ -795,17 +800,19 @@ let apply_on_clause (f,t) clause = | _ -> errorlabstrm "" (str "Ill-formed clause applicator.")) in clenv_fchain argmv f_clause clause -let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort = +let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort gl= let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (e,None,t) env in let discriminator = build_discriminator sigma e_env dirn (mkVar e) sort cpath in - let (pf, absurd_term) = discrimination_pf e (t,t1,t2) discriminator lbeq in + let (pf, absurd_term), eff = + discrimination_pf e (t,t1,t2) discriminator lbeq in let pf_ty = mkArrow eqn absurd_term in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = clenv_value_cast_meta absurd_clause in + let gl = {gl with eff = Declareops.union_side_effects eff gl.eff } in tclTHENS (cut_intro absurd_term) - [onLastHypId gen_absurdity; refine pf] + [onLastHypId gen_absurdity; refine pf] gl let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause gls = let sigma = eq_clause.evd in @@ -1134,7 +1141,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k) let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec" -let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) = +let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) gl = (* fetch the informations of the pair *) let ceq = constr_of_global Coqlib.glob_eq in let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in @@ -1153,19 +1160,19 @@ let inject_if_homogenous_dependent_pair env sigma (eq,_,(t,t1,t2)) = Library.require_library [Loc.ghost,eqdep_dec] (Some false); let inj2 = Coqlib.coq_constant "inj_pair2_eq_dec is missing" ["Logic";"Eqdep_dec"] "inj_pair2_eq_dec" in + let c, eff = find_scheme (!eq_dec_scheme_kind_name()) ind in + let gl = { gl with eff = Declareops.union_side_effects eff gl.eff } in (* cut with the good equality and prove the requested goal *) tclTHENS (cut (mkApp (ceq,new_eq_args))) [tclIDTAC; tclTHEN (apply ( - mkApp(inj2, - [|ar1.(0);mkConst (find_scheme (!eq_dec_scheme_kind_name()) ind); - ar1.(1);ar1.(2);ar1.(3);ar2.(3)|]) + mkApp(inj2,[|ar1.(0);mkConst c;ar1.(1);ar1.(2);ar1.(3);ar2.(3)|]) )) (Auto.trivial [] []) - ] + ] gl (* not a dep eq or no decidable type found *) end else raise Not_dep_pair -let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = +let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause gl = let sigma = eq_clause.evd in let env = eq_clause.env in match find_positions env sigma t1 t2 with @@ -1178,10 +1185,10 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause = | Inr [([],_,_)] when Flags.version_strictly_greater Flags.V8_3 -> errorlabstrm "Equality.inj" (str"Nothing to inject.") | Inr posns -> - try inject_if_homogenous_dependent_pair env sigma u + try inject_if_homogenous_dependent_pair env sigma u gl with e when (Errors.noncritical e || e = Not_dep_pair) -> inject_at_positions env sigma l2r u eq_clause posns - (tac (clenv_value eq_clause)) + (tac (clenv_value eq_clause)) gl let postInjEqTac ipats c n = match ipats with @@ -1255,7 +1262,7 @@ let swapEquandsInConcl gls = let bareRevSubstInConcl lbeq body (t,e1,e2) gls = (* find substitution scheme *) - let eq_elim = find_elim lbeq.eq (Some false) false None None gls in + let eq_elim, gls = find_elim lbeq.eq (Some false) false None None gls in (* build substitution predicate *) let p = lambda_create (pf_env gls) (t,body) in (* apply substitution scheme *) |