diff options
| -rw-r--r-- | tactics/equality.ml | 23 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 19 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.ml | 16 |
4 files changed, 32 insertions, 30 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 96b61b6994..65f23ab0e4 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1069,7 +1069,8 @@ let onEquality with_evars tac (c,lbindc) = let eq_clause = pf_apply make_clenv_binding gl (c,t') lbindc in let eq_clause' = Clenvtac.clenv_pose_dependent_evars ~with_evars eq_clause in let eqn = clenv_type eq_clause' in - let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in + (* FIXME evar leak *) + let (eq,u,eq_args) = pf_apply find_this_eq_data_decompose gl eqn in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') @@ -1341,7 +1342,7 @@ let inject_if_homogenous_dependent_pair ty = Proofview.Goal.enter begin fun gl -> try let sigma = Tacmach.New.project gl in - let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in + let eq,u,(t,t1,t2) = pf_apply find_this_eq_data_decompose gl ty in (* fetch the informations of the pair *) let sigTconstr = Coqlib.(lib_ref "core.sigT.type") in let existTconstr = Coqlib.lib_ref "core.sigT.intro" in @@ -1603,7 +1604,7 @@ let cutSubstInConcl l2r eqn = Proofview.Goal.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 (lbeq,u,(t,e1,e2)) = pf_apply 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)) = subst_tuple_term env sigma e1 e2 typ in @@ -1620,7 +1621,7 @@ let cutSubstInHyp l2r eqn id = Proofview.Goal.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 (lbeq,u,(t,e1,e2)) = pf_apply 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)) = subst_tuple_term env sigma e1 e2 typ in @@ -1715,7 +1716,7 @@ let is_eq_x gl x d = | _ -> false in let c = pf_nf_evar gl (NamedDecl.get_type d) in - let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in + let (_,lhs,rhs) = pi3 (pf_apply find_eq_data_decompose gl c) in if (is_var x lhs) && not (local_occur_var (project gl) x rhs) then raise (FoundHyp (id,rhs,true)); if (is_var x rhs) && not (local_occur_var (project gl) x lhs) then raise (FoundHyp (id,lhs,false)) with Constr_matching.PatternMatchingFailure -> @@ -1812,7 +1813,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let find_equations gl = let env = Proofview.Goal.env gl in let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let select_equation_name decl = try let lbeq,u,(_,x,y) = find_eq_data_decompose (NamedDecl.get_type decl) in @@ -1837,7 +1838,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = Proofview.Goal.enter begin fun gl -> let sigma = project gl in let env = Proofview.Goal.env gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let c = pf_get_hyp hyp gl |> NamedDecl.get_type in let _,_,(_,x,y) = find_eq_data_decompose c in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) @@ -1863,7 +1864,7 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let-ins *) Proofview.Goal.enter begin fun gl -> let sigma = project gl in - let find_eq_data_decompose = find_eq_data_decompose gl in + let find_eq_data_decompose = pf_apply find_eq_data_decompose gl in let test (_,c) = try let lbeq,u,(_,x,y) = find_eq_data_decompose c in @@ -1887,19 +1888,19 @@ let subst_all ?(flags=default_subst_tactic_flags) () = let cond_eq_term_left c t gl = try - let (_,x,_) = pi3 (find_eq_data_decompose gl t) in + let (_,x,_) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term_right c t gl = try - let (_,_,x) = pi3 (find_eq_data_decompose gl t) in + let (_,_,x) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then false else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" let cond_eq_term c t gl = try - let (_,x,y) = pi3 (find_eq_data_decompose gl t) in + let (_,x,y) = pi3 (pf_apply find_eq_data_decompose gl t) in if pf_conv_x gl c x then true else if pf_conv_x gl c y then false else failwith "not convertible" diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 90a9a7acd9..1f68117a76 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -19,7 +19,6 @@ open Inductiveops open Constr_matching open Coqlib open Declarations -open Tacmach.New open Context.Rel.Declaration module RelDecl = Context.Rel.Declaration @@ -452,26 +451,26 @@ let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) let hd,u = destInd sigma (fst (destApp sigma eqn)) in d,u,k -let extract_eq_args gl = function +let extract_eq_args env sigma = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_unsafe_type_of gl e1 in (t,e1,e2) + let t = Typing.unsafe_type_of env sigma e1 in (t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> - if pf_conv_x gl t1 t2 then (t1,e1,e2) + if Reductionops.is_conv env sigma t1 t2 then (t1,e1,e2) else raise PatternMatchingFailure -let find_eq_data_decompose gl eqn = - let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in - (lbeq,u,extract_eq_args gl eq_args) +let find_eq_data_decompose env sigma eqn = + let (lbeq,u,eq_args) = find_eq_data sigma eqn in + (lbeq,u,extract_eq_args env sigma eq_args) -let find_this_eq_data_decompose gl eqn = +let find_this_eq_data_decompose env sigma eqn = let (lbeq,u,eq_args) = try (*first_match (match_eq eqn) inversible_equalities*) - find_eq_data (project gl) eqn + find_eq_data sigma eqn with PatternMatchingFailure -> user_err (str "No primitive equality found.") in let eq_args = - try extract_eq_args gl eq_args + try extract_eq_args env sigma eq_args with PatternMatchingFailure -> user_err Pp.(str "Don't know what to do with JMeq on arguments not of same type.") in (lbeq,u,eq_args) diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 803305a1ca..0000f81d3f 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -122,11 +122,11 @@ val match_with_equation: (** Match terms [eq A t u], [identity A t u] or [JMeq A t A u] Returns associated lemmas and [A,t,u] or fails PatternMatchingFailure *) -val find_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** Idem but fails with an error message instead of PatternMatchingFailure *) -val find_this_eq_data_decompose : Proofview.Goal.t -> constr -> +val find_this_eq_data_decompose : Environ.env -> evar_map -> constr -> coq_eq_data * EInstance.t * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index ca66f4bce2..3a4a2dc814 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -2285,8 +2285,8 @@ let intro_decomp_eq_function = ref (fun _ -> failwith "Not implemented") let declare_intro_decomp_eq f = intro_decomp_eq_function := f -let my_find_eq_data_decompose gl t = - try Some (find_eq_data_decompose gl t) +let my_find_eq_data_decompose env sigma t = + try Some (find_eq_data_decompose env sigma t) with e when is_anomaly e (* Hack in case equality is not yet defined... one day, maybe, known equalities will be dynamically registered *) @@ -2296,13 +2296,15 @@ let my_find_eq_data_decompose gl t = let intro_decomp_eq ?loc l thin tac id = Proofview.Goal.enter begin fun gl -> let c = mkVar id in - let t = Tacmach.New.pf_unsafe_type_of gl c in - let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in - match my_find_eq_data_decompose gl t with + let env = Proofview.Goal.env gl in + let sigma = Proofview.Goal.sigma gl in + let sigma, t = Typing.type_of env sigma c in + let _,t = reduce_to_quantified_ind env sigma t in + match my_find_eq_data_decompose env sigma t with | Some (eq,u,eq_args) -> !intro_decomp_eq_function - (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) - (eq,t,eq_args) (c, t) + (fun n -> tac ((CAst.make id)::thin) (Some (true,n)) l) + (eq,t,eq_args) (c, t) | None -> Tacticals.New.tclZEROMSG (str "Not a primitive equality here.") end |