diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/contradiction.ml | 10 | ||||
| -rw-r--r-- | tactics/elim.ml | 4 | ||||
| -rw-r--r-- | tactics/eqdecide.ml | 12 | ||||
| -rw-r--r-- | tactics/equality.ml | 72 | ||||
| -rw-r--r-- | tactics/equality.mli | 4 | ||||
| -rw-r--r-- | tactics/hipattern.ml | 156 | ||||
| -rw-r--r-- | tactics/hipattern.mli | 24 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 38 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
10 files changed, 192 insertions, 132 deletions
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index 2058b95a6..a8be704b2 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -66,12 +66,12 @@ let contradiction_context = let id = NamedDecl.get_id d in let typ = nf_evar sigma (NamedDecl.get_type d) in let typ = whd_all env sigma (EConstr.of_constr typ) in - if is_empty_type sigma typ then + if is_empty_type sigma (EConstr.of_constr typ) then simplest_elim (mkVar id) else match kind_of_term typ with - | Prod (na,t,u) when is_empty_type sigma u -> + | Prod (na,t,u) when is_empty_type sigma (EConstr.of_constr u) -> let is_unit_or_eq = - if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma t + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type sigma (EConstr.of_constr t) else None in Tacticals.New.tclORELSE (match is_unit_or_eq with @@ -105,7 +105,7 @@ let is_negation_of env sigma typ t = match kind_of_term (whd_all env sigma t) with | Prod (na,t,u) -> let u = nf_evar sigma u in - is_empty_type sigma u && is_conv_leq env sigma (EConstr.of_constr typ) (EConstr.of_constr t) + is_empty_type sigma (EConstr.of_constr u) && is_conv_leq env sigma (EConstr.of_constr typ) (EConstr.of_constr t) | _ -> false let contradiction_term (c,lbind as cl) = @@ -115,7 +115,7 @@ let contradiction_term (c,lbind as cl) = let type_of = Tacmach.New.pf_unsafe_type_of gl in let typ = type_of (EConstr.of_constr c) in let _, ccl = splay_prod env sigma (EConstr.of_constr typ) in - if is_empty_type sigma ccl then + if is_empty_type sigma (EConstr.of_constr ccl) then Tacticals.New.tclTHEN (elim false None cl None) (Tacticals.New.tclTRY assumption) diff --git a/tactics/elim.ml b/tactics/elim.ml index fe36085b8..d00e504ff 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -108,12 +108,12 @@ let decompose_these c l = let decompose_and c = general_decompose - (fun sigma (_,t) -> is_record sigma t) + (fun sigma (_,t) -> is_record sigma (EConstr.of_constr t)) c let decompose_or c = general_decompose - (fun sigma (_,t) -> is_disjunction sigma t) + (fun sigma (_,t) -> is_disjunction sigma (EConstr.of_constr t)) c let h_decompose l c = decompose_these c l diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml index d1b14a907..ed81d748a 100644 --- a/tactics/eqdecide.ml +++ b/tactics/eqdecide.ml @@ -141,8 +141,8 @@ open Proofview.Notations (* spiwack: a small wrapper around [Hipattern]. *) -let match_eqdec c = - try Proofview.tclUNIT (match_eqdec c) +let match_eqdec sigma c = + try Proofview.tclUNIT (match_eqdec sigma c) with PatternMatchingFailure -> Proofview.tclZERO PatternMatchingFailure (* /spiwack *) @@ -171,7 +171,9 @@ let solveEqBranch rectype = begin Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in - match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) -> + let concl = EConstr.of_constr concl in + let sigma = project gl in + match_eqdec sigma concl >>= fun (eqonleft,op,lhs,rhs,_) -> let (mib,mip) = Global.lookup_inductive rectype in let nparams = mib.mind_nparams in let getargs l = List.skipn nparams (snd (decompose_app l)) in @@ -196,7 +198,9 @@ let decideGralEquality = begin Proofview.Goal.enter { enter = begin fun gl -> let concl = pf_nf_concl gl in - match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) -> + let concl = EConstr.of_constr concl in + let sigma = project gl in + match_eqdec sigma concl >>= fun (eqonleft,_,c1,c2,typ) -> let headtyp = hd_app (pf_compute gl (EConstr.of_constr typ)) in begin match kind_of_term headtyp with | Ind (mi,_) -> Proofview.tclUNIT mi diff --git a/tactics/equality.ml b/tactics/equality.ml index fa4164bb9..e1a8d2bdb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -448,8 +448,9 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac let env = Proofview.Goal.env gl in let ctype = get_type_of env sigma (EConstr.of_constr c) in let rels, t = decompose_prod_assum (whd_betaiotazeta sigma (EConstr.of_constr ctype)) in - match match_with_equality_type sigma t with + match match_with_equality_type sigma (EConstr.of_constr t) with | Some (hdcncl,args) -> (* Fast path: direct leibniz-like rewrite *) + let hdcncl = EConstr.Unsafe.to_constr hdcncl in let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t rels) l with_evars frzevars dep_proof_ok hdcncl @@ -464,8 +465,9 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac Proofview.tclEVARMAP >>= fun sigma -> let env' = push_rel_context rels env in let rels',t' = splay_prod_assum env' sigma (EConstr.of_constr t) in (* Search for underlying eq *) - match match_with_equality_type sigma t' with + match match_with_equality_type sigma (EConstr.of_constr t') with | Some (hdcncl,args) -> + let hdcncl = EConstr.Unsafe.to_constr hdcncl in let lft2rgt = adjust_rewriting_direction args lft2rgt in leibniz_rewrite_ebindings_clause cls lft2rgt tac c (it_mkProd_or_LetIn t' (rels' @ rels)) l with_evars frzevars dep_proof_ok hdcncl @@ -768,7 +770,7 @@ let find_positions env sigma t1 t2 = let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp] else [InSet;InType] in - Inr (findrec sorts [] (EConstr.of_constr t1) (EConstr.of_constr t2)) + Inr (findrec sorts [] t1 t2) with DiscrFound (path,c1,c2) -> Inl (path,c1,c2) @@ -943,7 +945,7 @@ let gen_absurdity id = Proofview.Goal.enter { enter = begin fun gl -> let sigma = project gl in let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in - let hyp_typ = pf_nf_evar gl hyp_typ in + let hyp_typ = EConstr.of_constr hyp_typ in if is_empty_type sigma hyp_typ then simplest_elim (mkVar id) @@ -991,6 +993,9 @@ let apply_on_clause (f,t) clause = clenv_fchain ~with_univs:false argmv f_clause clause let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = + let t = EConstr.Unsafe.to_constr t in + let t1 = EConstr.Unsafe.to_constr t1 in + let t2 = EConstr.Unsafe.to_constr t2 in let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (e,t)) env in let discriminator = @@ -1029,7 +1034,7 @@ let onEquality with_evars tac (c,lbindc) = let eq_clause' = Clenvtac.clenv_pose_dependent_evars with_evars eq_clause in let eqn = clenv_type eq_clause' in let eqn = EConstr.Unsafe.to_constr eqn in - let (eq,u,eq_args) = find_this_eq_data_decompose gl eqn in + let (eq,u,eq_args) = find_this_eq_data_decompose gl (EConstr.of_constr eqn) in tclTHEN (Proofview.Unsafe.tclEVARS eq_clause'.evd) (tac (eq,eqn,eq_args) eq_clause') @@ -1041,7 +1046,7 @@ let onNegatedEquality with_evars tac = let ccl = Proofview.Goal.concl gl in let env = Proofview.Goal.env gl in match kind_of_term (hnf_constr env sigma (EConstr.of_constr ccl)) with - | Prod (_,t,u) when is_empty_type sigma u -> + | Prod (_,t,u) when is_empty_type sigma (EConstr.of_constr u) -> tclTHEN introf (onLastHypId (fun id -> onEquality with_evars tac (mkVar id,NoBindings))) @@ -1320,6 +1325,7 @@ let inject_if_homogenous_dependent_pair ty = try let sigma = Tacmach.New.project gl in let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in + let t = EConstr.Unsafe.to_constr t in (* fetch the informations of the pair *) let ceq = Universes.constr_of_global Coqlib.glob_eq in let sigTconstr () = (Coqlib.build_sigma_type()).Coqlib.typ in @@ -1327,8 +1333,8 @@ let inject_if_homogenous_dependent_pair ty = (* check whether the equality deals with dep pairs or not *) let eqTypeDest = fst (decompose_app t) in if not (Globnames.is_global (sigTconstr()) eqTypeDest) then raise Exit; - let hd1,ar1 = decompose_app_vect sigma (EConstr.of_constr t1) and - hd2,ar2 = decompose_app_vect sigma (EConstr.of_constr t2) in + let hd1,ar1 = decompose_app_vect sigma t1 and + hd2,ar2 = decompose_app_vect sigma t2 in if not (Globnames.is_global (existTconstr()) hd1) then raise Exit; if not (Globnames.is_global (existTconstr()) hd2) then raise Exit; let ind,_ = try pf_apply find_mrectype gl (EConstr.of_constr ar1.(0)) with Not_found -> raise Exit in @@ -1369,6 +1375,9 @@ let simplify_args env sigma t = | _ -> t let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = + let t = EConstr.Unsafe.to_constr t in + let t1 = EConstr.Unsafe.to_constr t1 in + let t2 = EConstr.Unsafe.to_constr t2 in let e = next_ident_away eq_baseid (ids_of_context env) in let e_env = push_named (LocalAssum (e,t)) env in let evdref = ref sigma in @@ -1396,7 +1405,7 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac = (Tacticals.New.tclTHENFIRST (Proofview.tclIGNORE (Proofview.Monad.List.map (fun (pf,ty) -> tclTHENS (cut ty) - [inject_if_homogenous_dependent_pair ty; + [inject_if_homogenous_dependent_pair (EConstr.of_constr ty); Proofview.V82.tactic (Tacmach.refine (EConstr.of_constr pf))]) (if l2r then List.rev injectors else injectors))) (tac (List.length injectors))) @@ -1536,7 +1545,12 @@ let decomp_tuple_term env sigma c t = let rec decomprec inner_code ex exty = let iterated_decomp = try - let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose ex in + let ex = EConstr.of_constr ex in + let ({proj1=p1; proj2=p2}),(i,a,p,car,cdr) = find_sigma_data_decompose sigma ex in + let a = EConstr.Unsafe.to_constr a in + let p = EConstr.Unsafe.to_constr p in + let car = EConstr.Unsafe.to_constr car in + let cdr = EConstr.Unsafe.to_constr cdr in let car_code = applist (mkConstU (destConstRef p1,i),[a;p;inner_code]) and cdr_code = applist (mkConstU (destConstRef p2,i),[a;p;inner_code]) in let cdrtyp = beta_applist sigma (EConstr.of_constr p,[EConstr.of_constr car]) in @@ -1547,6 +1561,8 @@ let decomp_tuple_term env sigma c t = in decomprec (mkRel 1) c t let subst_tuple_term env sigma dep_pair1 dep_pair2 b = + let dep_pair1 = EConstr.Unsafe.to_constr dep_pair1 in + let dep_pair2 = EConstr.Unsafe.to_constr dep_pair2 in let sigma = Sigma.to_evar_map sigma in let typ = get_type_of env sigma (EConstr.of_constr dep_pair1) in (* We find all possible decompositions *) @@ -1583,7 +1599,7 @@ 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 (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl (EConstr.of_constr eqn) in let typ = pf_concl gl in let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in let Sigma ((typ, expected), sigma, p) = subst_tuple_term env sigma e1 e2 typ in @@ -1602,7 +1618,7 @@ let cutSubstInHyp l2r eqn id = 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 (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl (EConstr.of_constr 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), sigma, p) = subst_tuple_term env sigma e1 e2 typ in @@ -1682,20 +1698,21 @@ let restrict_to_eq_and_identity eq = (* compatibility *) not (is_global glob_identity eq) then raise Constr_matching.PatternMatchingFailure -exception FoundHyp of (Id.t * constr * bool) +exception FoundHyp of (Id.t * EConstr.constr * bool) (* tests whether hyp [c] is [x = t] or [t = x], [x] not occurring in [t] *) let is_eq_x gl x d = let id = NamedDecl.get_id d in try - let is_var id c = match kind_of_term c with + let is_var id c = match EConstr.kind (project gl) c with | Var id' -> Id.equal id id' | _ -> false in let c = pf_nf_evar gl (NamedDecl.get_type d) in + let c = EConstr.of_constr c in let (_,lhs,rhs) = pi3 (find_eq_data_decompose gl c) in - if (is_var x lhs) && not (local_occur_var (project gl) x (EConstr.of_constr rhs)) then raise (FoundHyp (id,rhs,true)); - if (is_var x rhs) && not (local_occur_var (project gl) x (EConstr.of_constr lhs)) then raise (FoundHyp (id,lhs,false)) + 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 -> () @@ -1753,7 +1770,7 @@ let subst_one_var dep_proof_ok x = user_err ~hdr:"Subst" (str "Cannot find any non-recursive equality over " ++ pr_id x ++ str".") - with FoundHyp res -> res in + with FoundHyp (id, c, b) -> (id, EConstr.Unsafe.to_constr c, b) in subst_one dep_proof_ok x res end } @@ -1788,7 +1805,9 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let find_eq_data_decompose = 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 + let lbeq,u,(_,x,y) = find_eq_data_decompose (EConstr.of_constr (NamedDecl.get_type decl)) in + let x = EConstr.Unsafe.to_constr x in + let y = EConstr.Unsafe.to_constr y in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; match kind_of_term x, kind_of_term y with @@ -1812,7 +1831,10 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let env = Proofview.Goal.env gl in let find_eq_data_decompose = find_eq_data_decompose gl in let c = pf_get_hyp hyp gl |> NamedDecl.get_type in + let c = EConstr.of_constr c in let _,_,(_,x,y) = find_eq_data_decompose c in + let x = EConstr.Unsafe.to_constr x in + let y = EConstr.Unsafe.to_constr y in (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if Term.eq_constr x y then Proofview.tclUNIT () else match kind_of_term x, kind_of_term y with @@ -1838,7 +1860,10 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let find_eq_data_decompose = find_eq_data_decompose gl in let test (_,c) = try + let c = EConstr.of_constr c in let lbeq,u,(_,x,y) = find_eq_data_decompose c in + let x = EConstr.Unsafe.to_constr x in + let y = EConstr.Unsafe.to_constr y in let eq = Universes.constr_of_global_univ (lbeq.eq,u) in if flags.only_leibniz then restrict_to_eq_and_identity eq; (* J.F.: added to prevent failure on goal containing x=x as an hyp *) @@ -1858,21 +1883,24 @@ let subst_all ?(flags=default_subst_tactic_flags ()) () = let cond_eq_term_left c t gl = try + let t = EConstr.of_constr t in let (_,x,_) = pi3 (find_eq_data_decompose gl t) in - if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true else failwith "not convertible" + if pf_conv_x gl (EConstr.of_constr 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 t = EConstr.of_constr t in let (_,_,x) = pi3 (find_eq_data_decompose gl t) in - if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then false else failwith "not convertible" + if pf_conv_x gl (EConstr.of_constr 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 t = EConstr.of_constr t in let (_,x,y) = pi3 (find_eq_data_decompose gl t) in - if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr x) then true - else if pf_conv_x gl (EConstr.of_constr c) (EConstr.of_constr y) then false + if pf_conv_x gl (EConstr.of_constr c) x then true + else if pf_conv_x gl (EConstr.of_constr c) y then false else failwith "not convertible" with Constr_matching.PatternMatchingFailure -> failwith "not an equality" diff --git a/tactics/equality.mli b/tactics/equality.mli index 6a4a8126e..779d1e9b2 100644 --- a/tactics/equality.mli +++ b/tactics/equality.mli @@ -96,8 +96,8 @@ val cutRewriteInConcl : bool -> constr -> unit Proofview.tactic val rewriteInHyp : bool -> constr -> Id.t -> unit Proofview.tactic val rewriteInConcl : bool -> constr -> unit Proofview.tactic -val discriminable : env -> evar_map -> constr -> constr -> bool -val injectable : env -> evar_map -> constr -> constr -> bool +val discriminable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool +val injectable : env -> evar_map -> EConstr.constr -> EConstr.constr -> bool (* Subst *) diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 5d78fd585..6681e5e49 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -12,6 +12,7 @@ open Util open Names open Term open Termops +open EConstr open Inductiveops open Constr_matching open Coqlib @@ -31,9 +32,9 @@ module RelDecl = Context.Rel.Declaration -- Eduardo (6/8/97). *) -type 'a matching_function = Evd.evar_map -> constr -> 'a option +type 'a matching_function = Evd.evar_map -> EConstr.constr -> 'a option -type testing_function = Evd.evar_map -> constr -> bool +type testing_function = Evd.evar_map -> EConstr.constr -> bool let mkmeta n = Nameops.make_ident "X" (Some n) let meta1 = mkmeta 1 @@ -44,10 +45,10 @@ let meta4 = mkmeta 4 let op2bool = function Some _ -> true | None -> false let match_with_non_recursive_type sigma t = - match kind_of_term t with + match EConstr.kind sigma t with | App _ -> - let (hdapp,args) = decompose_app t in - (match kind_of_term hdapp with + let (hdapp,args) = decompose_app sigma t in + (match EConstr.kind sigma hdapp with | Ind (ind,u) -> if (Global.lookup_mind (fst ind)).mind_finite == Decl_kinds.CoFinite then Some (hdapp,args) @@ -64,9 +65,9 @@ let is_non_recursive_type sigma t = op2bool (match_with_non_recursive_type sigma since they may appear in types of inductive constructors (see #2629) *) let rec has_nodep_prod_after n sigma c = - match kind_of_term c with + match EConstr.kind sigma c with | Prod (_,_,b) | LetIn (_,_,_,b) -> - ( n>0 || EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b)) + ( n>0 || Vars.noccurn sigma 1 b) && (has_nodep_prod_after (n-1) sigma b) | _ -> true @@ -87,9 +88,11 @@ let is_lax_conjunction = function | Some false -> true | _ -> false +let prod_assum sigma t = fst (decompose_prod_assum sigma t) + let match_with_one_constructor sigma style onlybinary allow_rec t = - let (hdapp,args) = decompose_app t in - let res = match kind_of_term hdapp with + let (hdapp,args) = decompose_app sigma t in + let res = match EConstr.kind sigma hdapp with | Ind ind -> let (mib,mip) = Global.lookup_inductive (fst ind) in if Int.equal (Array.length mip.mind_consnames) 1 @@ -98,22 +101,23 @@ let match_with_one_constructor sigma style onlybinary allow_rec t = then if is_strict_conjunction style (* strict conjunction *) then let ctx = - (prod_assum (snd - (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in + (prod_assum sigma (snd + (decompose_prod_n_assum sigma mib.mind_nparams (EConstr.of_constr mip.mind_nf_lc.(0))))) in if List.for_all (fun decl -> let c = RelDecl.get_type decl in is_local_assum decl && - isRel c && - Int.equal (destRel c) mib.mind_nparams) ctx + Term.isRel c && + Int.equal (Term.destRel c) mib.mind_nparams) ctx then Some (hdapp,args) else None else - let ctyp = Term.prod_applist mip.mind_nf_lc.(0) args in - let cargs = List.map RelDecl.get_type (prod_assum ctyp) in + let ctyp = Termops.prod_applist sigma (EConstr.of_constr mip.mind_nf_lc.(0)) args in + let cargs = List.map RelDecl.get_type (prod_assum sigma ctyp) in if not (is_lax_conjunction style) || has_nodep_prod sigma ctyp then (* Record or non strict conjunction *) + let cargs = List.map EConstr.of_constr cargs in Some (hdapp,List.rev cargs) else None @@ -140,7 +144,7 @@ let is_record sigma t = let match_with_tuple sigma t = let t = match_with_one_constructor sigma None false true t in Option.map (fun (hd,l) -> - let ind = destInd hd in + let ind = destInd sigma hd in let (mib,mip) = Global.lookup_pinductive ind in let isrec = mis_is_recursive (fst ind,mib,mip) in (hd,l,isrec)) t @@ -154,14 +158,15 @@ let is_tuple sigma t = "Inductive I A1 ... An := C1 (_:A1) | ... | Cn : (_:An)" *) let test_strict_disjunction n lc = + let open Term in Array.for_all_i (fun i c -> match (prod_assum (snd (decompose_prod_n_assum n c))) with | [LocalAssum (_,c)] -> isRel c && Int.equal (destRel c) (n - i) | _ -> false) 0 lc let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = - let (hdapp,args) = decompose_app t in - let res = match kind_of_term hdapp with + let (hdapp,args) = decompose_app sigma t in + let res = match EConstr.kind sigma hdapp with | Ind (ind,u) -> let car = constructors_nrealargs ind in let (mib,mip) = Global.lookup_inductive ind in @@ -176,7 +181,7 @@ let match_with_disjunction ?(strict=false) ?(onlybinary=false) sigma t = None else let cargs = - Array.map (fun ar -> pi2 (destProd (Term.prod_applist ar args))) + Array.map (fun ar -> pi2 (destProd sigma (prod_applist sigma (EConstr.of_constr ar) args))) mip.mind_nf_lc in Some (hdapp,Array.to_list cargs) else @@ -194,8 +199,8 @@ let is_disjunction ?(strict=false) ?(onlybinary=false) sigma t = constructors *) let match_with_empty_type sigma t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with + let (hdapp,args) = decompose_app sigma t in + match EConstr.kind sigma hdapp with | Ind ind -> let (mib,mip) = Global.lookup_pinductive ind in let nconstr = Array.length mip.mind_consnames in @@ -208,8 +213,8 @@ let is_empty_type sigma t = op2bool (match_with_empty_type sigma t) Parameters and indices are allowed *) let match_with_unit_or_eq_type sigma t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with + let (hdapp,args) = decompose_app sigma t in + match EConstr.kind sigma hdapp with | Ind ind -> let (mib,mip) = Global.lookup_pinductive ind in let constr_types = mip.mind_nf_lc in @@ -276,13 +281,13 @@ let coq_refl_jm_pattern = open Globnames -let is_matching x y = is_matching (Global.env ()) Evd.empty x (EConstr.of_constr y) -let matches x y = matches (Global.env ()) Evd.empty x (EConstr.of_constr y) +let is_matching sigma x y = is_matching (Global.env ()) sigma x y +let matches sigma x y = matches (Global.env ()) sigma x y -let match_with_equation t = - if not (isApp t) then raise NoEquationFound; - let (hdapp,args) = destApp t in - match kind_of_term hdapp with +let match_with_equation sigma t = + if not (isApp sigma t) then raise NoEquationFound; + let (hdapp,args) = destApp sigma t in + match EConstr.kind sigma hdapp with | Ind (ind,u) -> if eq_gr (IndRef ind) glob_eq then Some (build_coq_eq_data()),hdapp, @@ -298,11 +303,11 @@ let match_with_equation t = let constr_types = mip.mind_nf_lc in let nconstr = Array.length mip.mind_consnames in if Int.equal nconstr 1 then - if is_matching coq_refl_leibniz1_pattern constr_types.(0) then + if is_matching sigma coq_refl_leibniz1_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, MonomorphicLeibnizEq(args.(0),args.(1)) - else if is_matching coq_refl_leibniz2_pattern constr_types.(0) then + else if is_matching sigma coq_refl_leibniz2_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, PolymorphicLeibnizEq(args.(0),args.(1),args.(2)) - else if is_matching coq_refl_jm_pattern constr_types.(0) then + else if is_matching sigma coq_refl_jm_pattern (EConstr.of_constr constr_types.(0)) then None, hdapp, HeterogenousEq(args.(0),args.(1),args.(2),args.(3)) else raise NoEquationFound else raise NoEquationFound @@ -319,8 +324,8 @@ let is_inductive_equality ind = Int.equal nconstr 1 && Int.equal (constructor_nrealargs (ind,1)) 0 let match_with_equality_type sigma t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with + let (hdapp,args) = decompose_app sigma t in + match EConstr.kind sigma hdapp with | Ind (ind,_) when is_inductive_equality ind -> Some (hdapp,args) | _ -> None @@ -331,23 +336,25 @@ let is_equality_type sigma t = op2bool (match_with_equality_type sigma t) (** X1 -> X2 **) let coq_arrow_pattern = mkPattern (mkGArrow (mkGPatVar "X1") (mkGPatVar "X2")) -let match_arrow_pattern t = - let result = matches coq_arrow_pattern t in +let match_arrow_pattern sigma t = + let result = matches sigma coq_arrow_pattern t in match Id.Map.bindings result with | [(m1,arg);(m2,mind)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2); (arg, mind) | _ -> anomaly (Pp.str "Incorrect pattern matching") let match_with_imp_term sigma c = - match kind_of_term c with - | Prod (_,a,b) when EConstr.Vars.noccurn sigma 1 (EConstr.of_constr b) -> Some (a,b) + match EConstr.kind sigma c with + | Prod (_,a,b) when Vars.noccurn sigma 1 b -> Some (a,b) | _ -> None let is_imp_term sigma c = op2bool (match_with_imp_term sigma c) let match_with_nottype sigma t = try - let (arg,mind) = match_arrow_pattern t in + let (arg,mind) = match_arrow_pattern sigma t in + let arg = EConstr.of_constr arg in + let mind = EConstr.of_constr mind in if is_empty_type sigma mind then Some (mind,arg) else None with PatternMatchingFailure -> None @@ -356,19 +363,19 @@ let is_nottype sigma t = op2bool (match_with_nottype sigma t) (* Forall *) let match_with_forall_term sigma c= - match kind_of_term c with + match EConstr.kind sigma c with | Prod (nam,a,b) -> Some (nam,a,b) | _ -> None let is_forall_term sigma c = op2bool (match_with_forall_term sigma c) let match_with_nodep_ind sigma t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with + let (hdapp,args) = decompose_app sigma t in + match EConstr.kind sigma hdapp with | Ind ind -> let (mib,mip) = Global.lookup_pinductive ind in if Array.length (mib.mind_packets)>1 then None else - let nodep_constr = has_nodep_prod_after mib.mind_nparams sigma in + let nodep_constr c = has_nodep_prod_after mib.mind_nparams sigma (EConstr.of_constr c) in if Array.for_all nodep_constr mip.mind_nf_lc then let params= if Int.equal mip.mind_nrealargs 0 then args else @@ -381,14 +388,14 @@ let match_with_nodep_ind sigma t = let is_nodep_ind sigma t = op2bool (match_with_nodep_ind sigma t) let match_with_sigma_type sigma t = - let (hdapp,args) = decompose_app t in - match (kind_of_term hdapp) with + let (hdapp,args) = decompose_app sigma t in + match EConstr.kind sigma hdapp with | Ind ind -> let (mib,mip) = Global.lookup_pinductive ind in if Int.equal (Array.length (mib.mind_packets)) 1 && (Int.equal mip.mind_nrealargs 0) && (Int.equal (Array.length mip.mind_consnames)1) && - has_nodep_prod_after (mib.mind_nparams+1) sigma mip.mind_nf_lc.(0) then + has_nodep_prod_after (mib.mind_nparams+1) sigma (EConstr.of_constr mip.mind_nf_lc.(0)) then (*allowing only 1 existential*) Some (hdapp,args) else @@ -408,17 +415,17 @@ let rec first_match matcher = function (*** Equality *) -let match_eq eqn (ref, hetero) = +let match_eq sigma eqn (ref, hetero) = let ref = try Lazy.force ref with e when CErrors.noncritical e -> raise PatternMatchingFailure in - match kind_of_term eqn with + match EConstr.kind sigma eqn with | App (c, [|t; x; y|]) -> - if not hetero && is_global ref c then PolymorphicLeibnizEq (t, x, y) + if not hetero && Termops.is_global sigma ref c then PolymorphicLeibnizEq (t, x, y) else raise PatternMatchingFailure | App (c, [|t; x; t'; x'|]) -> - if hetero && is_global ref c then HeterogenousEq (t, x, t', x') + if hetero && Termops.is_global sigma ref c then HeterogenousEq (t, x, t', x') else raise PatternMatchingFailure | _ -> raise PatternMatchingFailure @@ -430,27 +437,27 @@ let equalities = (coq_jmeq_ref, true), check_jmeq_loaded, build_coq_jmeq_data; (coq_identity_ref, false), no_check, build_coq_identity_data] -let find_eq_data eqn = (* fails with PatternMatchingFailure *) - let d,k = first_match (match_eq eqn) equalities in - let hd,u = destInd (fst (destApp eqn)) in +let find_eq_data sigma eqn = (* fails with PatternMatchingFailure *) + let d,k = first_match (match_eq sigma eqn) equalities in + let hd,u = destInd sigma (fst (destApp sigma eqn)) in d,u,k let extract_eq_args gl = function | MonomorphicLeibnizEq (e1,e2) -> - let t = pf_unsafe_type_of gl (EConstr.of_constr e1) in (t,e1,e2) + let t = pf_unsafe_type_of gl e1 in (EConstr.of_constr t,e1,e2) | PolymorphicLeibnizEq (t,e1,e2) -> (t,e1,e2) | HeterogenousEq (t1,e1,t2,e2) -> - if pf_conv_x gl (EConstr.of_constr t1) (EConstr.of_constr t2) then (t1,e1,e2) + if pf_conv_x gl t1 t2 then (t1,e1,e2) else raise PatternMatchingFailure let find_eq_data_decompose gl eqn = - let (lbeq,u,eq_args) = find_eq_data eqn in + let (lbeq,u,eq_args) = find_eq_data (project gl) eqn in (lbeq,u,extract_eq_args gl eq_args) let find_this_eq_data_decompose gl eqn = let (lbeq,u,eq_args) = try (*first_match (match_eq eqn) inversible_equalities*) - find_eq_data eqn + find_eq_data (project gl) eqn with PatternMatchingFailure -> user_err (str "No primitive equality found.") in let eq_args = @@ -463,7 +470,6 @@ let match_eq_nf gls eqn (ref, hetero) = let n = if hetero then 4 else 3 in let args = List.init n (fun i -> mkGPatVar ("X" ^ string_of_int (i + 1))) in let pat = mkPattern (mkGAppRef ref args) in - let eqn = EConstr.of_constr eqn in match Id.Map.bindings (pf_matches gls pat eqn) with | [(m1,t);(m2,x);(m3,y)] -> assert (Id.equal m1 meta1 && Id.equal m2 meta2 && Id.equal m3 meta3); @@ -478,12 +484,12 @@ let dest_nf_eq gls eqn = (*** Sigma-types *) -let match_sigma ex = - match kind_of_term ex with - | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_exist_ref) f -> - build_sigma (), (snd (destConstruct f), a, p, car, cdr) - | App (f, [| a; p; car; cdr |]) when is_global (Lazy.force coq_existT_ref) f -> - build_sigma_type (), (snd (destConstruct f), a, p, car, cdr) +let match_sigma sigma ex = + match EConstr.kind sigma ex with + | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_exist_ref) f -> + build_sigma (), (snd (destConstruct sigma f), a, p, car, cdr) + | App (f, [| a; p; car; cdr |]) when Termops.is_global sigma (Lazy.force coq_existT_ref) f -> + build_sigma_type (), (snd (destConstruct sigma f), a, p, car, cdr) | _ -> raise PatternMatchingFailure let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) @@ -493,12 +499,12 @@ let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *) let coq_sig_pattern = lazy (mkPattern (mkGAppRef coq_sig_ref [mkGPatVar "X1"; mkGPatVar "X2"])) -let match_sigma t = - match Id.Map.bindings (matches (Lazy.force coq_sig_pattern) t) with - | [(_,a); (_,p)] -> (a,p) +let match_sigma sigma t = + match Id.Map.bindings (matches sigma (Lazy.force coq_sig_pattern) t) with + | [(_,a); (_,p)] -> (EConstr.of_constr a,EConstr.of_constr p) | _ -> anomaly (Pp.str "Unexpected pattern") -let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t +let is_matching_sigma sigma t = is_matching sigma (Lazy.force coq_sig_pattern) t (*** Decidable equalities *) @@ -530,15 +536,15 @@ let coq_eqdec_rev_pattern = coq_eqdec ~sum:coq_or_ref ~rev:true let op_or = coq_or_ref let op_sum = coq_sumbool_ref -let match_eqdec t = +let match_eqdec sigma t = let eqonleft,op,subst = - try true,op_sum,matches (Lazy.force coq_eqdec_inf_pattern) t + try true,op_sum,matches sigma (Lazy.force coq_eqdec_inf_pattern) t with PatternMatchingFailure -> - try false,op_sum,matches (Lazy.force coq_eqdec_inf_rev_pattern) t + try false,op_sum,matches sigma (Lazy.force coq_eqdec_inf_rev_pattern) t with PatternMatchingFailure -> - try true,op_or,matches (Lazy.force coq_eqdec_pattern) t + try true,op_or,matches sigma (Lazy.force coq_eqdec_pattern) t with PatternMatchingFailure -> - false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in + false,op_or,matches sigma (Lazy.force coq_eqdec_rev_pattern) t in match Id.Map.bindings subst with | [(_,typ);(_,c1);(_,c2)] -> eqonleft, Universes.constr_of_global (Lazy.force op), c1, c2, typ @@ -548,8 +554,8 @@ let match_eqdec t = let coq_not_pattern = lazy (mkPattern (mkGAppRef coq_not_ref [mkGHole])) let coq_imp_False_pattern = lazy (mkPattern (mkGArrow mkGHole (mkGRef coq_False_ref))) -let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t -let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t +let is_matching_not sigma t = is_matching sigma (Lazy.force coq_not_pattern) t +let is_matching_imp_False sigma t = is_matching sigma (Lazy.force coq_imp_False_pattern) t (* Remark: patterns that have references to the standard library must be evaluated lazily (i.e. at the time they are used, not a the time diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli index 8a453bf31..094d62df6 100644 --- a/tactics/hipattern.mli +++ b/tactics/hipattern.mli @@ -8,6 +8,8 @@ open Names open Term +open Evd +open EConstr open Coqlib (** High-order patterns *) @@ -40,8 +42,8 @@ open Coqlib also work on ad-hoc disjunctions introduced by the user. (Eduardo, 6/8/97). *) -type 'a matching_function = Evd.evar_map -> constr -> 'a option -type testing_function = Evd.evar_map -> constr -> bool +type 'a matching_function = evar_map -> constr -> 'a option +type testing_function = evar_map -> constr -> bool val match_with_non_recursive_type : (constr * constr list) matching_function val is_non_recursive_type : testing_function @@ -113,7 +115,7 @@ type equation_kind = exception NoEquationFound val match_with_equation: - constr -> coq_eq_data option * constr * equation_kind + evar_map -> constr -> coq_eq_data option * constr * equation_kind (***** Destructing patterns bound to some theory *) @@ -127,25 +129,25 @@ val find_this_eq_data_decompose : ([ `NF ], 'r) Proofview.Goal.t -> constr -> coq_eq_data * Univ.universe_instance * (types * constr * constr) (** A variant that returns more informative structure on the equality found *) -val find_eq_data : constr -> coq_eq_data * Univ.universe_instance * equation_kind +val find_eq_data : evar_map -> constr -> coq_eq_data * Univ.universe_instance * equation_kind (** Match a term of the form [(existT A P t p)] Returns associated lemmas and [A,P,t,p] *) -val find_sigma_data_decompose : constr -> +val find_sigma_data_decompose : evar_map -> constr -> coq_sigma_data * (Univ.universe_instance * constr * constr * constr * constr) (** Match a term of the form [{x:A|P}], returns [A] and [P] *) -val match_sigma : constr -> constr * constr +val match_sigma : evar_map -> constr -> constr * constr -val is_matching_sigma : constr -> bool +val is_matching_sigma : evar_map -> constr -> bool (** Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns [t,u,T] and a boolean telling if equality is on the left side *) -val match_eqdec : constr -> bool * constr * constr * constr * constr +val match_eqdec : evar_map -> constr -> bool * Constr.constr * Constr.constr * Constr.constr * Constr.constr (** Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *) -val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (constr * constr * constr) +val dest_nf_eq : ([ `NF ], 'r) Proofview.Goal.t -> constr -> (Constr.constr * Constr.constr * Constr.constr) (** Match a negation *) -val is_matching_not : constr -> bool -val is_matching_imp_False : constr -> bool +val is_matching_not : evar_map -> constr -> bool +val is_matching_imp_False : evar_map -> constr -> bool diff --git a/tactics/inv.ml b/tactics/inv.ml index 60f1c3542..a971b9356 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -341,7 +341,7 @@ let projectAndApply as_mode thin avoid id eqname names depids = Proofview.Goal.nf_enter { enter = begin fun gl -> (** We only look at the type of hypothesis "id" *) let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in - let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in + let (t,t1,t2) = Hipattern.dest_nf_eq gl (EConstr.of_constr hyp) in match (kind_of_term t1, kind_of_term t2) with | Var id1, _ -> generalizeRewriteIntros as_mode (subst_hyp true id) depids id1 | _, Var id2 -> generalizeRewriteIntros as_mode (subst_hyp false id) depids id2 diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f262aefa7..a04fb7ca2 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1654,11 +1654,12 @@ let descend_in_conjunctions avoid tac (err, info) c = let t = EConstr.of_constr t in let ((ind,u),t) = reduce_to_quantified_ind env sigma t in let sign,ccl = decompose_prod_assum t in + let ccl = EConstr.of_constr ccl in match match_with_tuple sigma ccl with | Some (_,_,isrec) -> let n = (constructors_nrealargs ind).(0) in let sort = Tacticals.New.elimination_sort_of_goal gl in - let IndType (indf,_) = find_rectype env sigma (EConstr.of_constr ccl) in + let IndType (indf,_) = find_rectype env sigma ccl in let (_,inst), params = dest_ind_family indf in let cstr = (get_constructors env indf).(0) in let elim = @@ -2324,7 +2325,7 @@ let intro_decomp_eq loc l thin tac id = let t = Tacmach.New.pf_unsafe_type_of gl (EConstr.of_constr c) in let t = EConstr.of_constr t in let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in - match my_find_eq_data_decompose gl t with + match my_find_eq_data_decompose gl (EConstr.of_constr t) with | Some (eq,u,eq_args) -> !intro_decomp_eq_function (fun n -> tac ((dloc,id)::thin) (Some (true,n)) l) @@ -2363,8 +2364,11 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = let type_of = Tacmach.New.pf_unsafe_type_of gl in let whd_all = Tacmach.New.pf_apply whd_all gl in let t = whd_all (EConstr.of_constr (type_of (EConstr.mkVar id))) in + let t = EConstr.of_constr t in let eqtac, thin = match match_with_equality_type sigma t with | Some (hdcncl,[_;lhs;rhs]) -> + let lhs = EConstr.Unsafe.to_constr lhs in + let rhs = EConstr.Unsafe.to_constr rhs in if l2r && isVar lhs && not (occur_var env sigma (destVar lhs) (EConstr.of_constr rhs)) then let id' = destVar lhs in subst_on l2r id' rhs, early_clear id' thin @@ -2375,6 +2379,7 @@ let rewrite_hyp_then assert_style with_evars thin l2r id tac = Tacticals.New.tclTHEN (rew_on l2r onConcl) (clear [id]), thin | Some (hdcncl,[c]) -> + let c = EConstr.Unsafe.to_constr c in let l2r = not l2r in (* equality of the form eq_true *) if isVar c then let id' = destVar c in @@ -4689,6 +4694,7 @@ let reflexivity_red allowred = inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in + let concl = EConstr.of_constr concl in match match_with_equality_type sigma concl with | None -> Proofview.tclZERO NoEquationFound | Some _ -> one_constructor 1 NoBindings @@ -4716,19 +4722,21 @@ let (forward_setoid_symmetry, setoid_symmetry) = Hook.make () (* This is probably not very useful any longer *) let prove_symmetry hdcncl eq_kind = let symc = + let open EConstr in match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> mkApp(hdcncl,[|c2;c1|]) | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp(hdcncl,[|typ;c2;c1|]) | HeterogenousEq (t1,c1,t2,c2) -> mkApp(hdcncl,[|t2;c2;t1;c1|]) in + let symc = EConstr.Unsafe.to_constr symc in Tacticals.New.tclTHENFIRST (cut symc) (Tacticals.New.tclTHENLIST [ intro; Tacticals.New.onLastHyp simplest_case; one_constructor 1 NoBindings ]) -let match_with_equation c = +let match_with_equation sigma c = try - let res = match_with_equation c in + let res = match_with_equation sigma c in Proofview.tclUNIT res with NoEquationFound -> Proofview.tclZERO NoEquationFound @@ -4738,8 +4746,9 @@ let symmetry_red allowred = (* PL: usual symmetry don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation concl >>= fun with_eqn -> + match_with_equation sigma (EConstr.of_constr concl) >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN @@ -4761,15 +4770,20 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make () let symmetry_in id = Proofview.Goal.enter { enter = begin fun gl -> + let sigma = Tacmach.New.project gl in let ctype = Tacmach.New.pf_unsafe_type_of gl (EConstr.mkVar id) in let sign,t = decompose_prod_assum ctype in + let t = EConstr.of_constr t in Proofview.tclORELSE begin - match_with_equation t >>= fun (_,hdcncl,eq) -> - let symccl = match eq with + match_with_equation sigma t >>= fun (_,hdcncl,eq) -> + let symccl = + let open EConstr in + match eq with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c2; c1 |]) | PolymorphicLeibnizEq (typ,c1,c2) -> mkApp (hdcncl, [| typ; c2; c1 |]) | HeterogenousEq (t1,c1,t2,c2) -> mkApp (hdcncl, [| t2; c2; t1; c1 |]) in + let symccl = EConstr.Unsafe.to_constr symccl in Tacticals.New.tclTHENS (cut (it_mkProd_or_LetIn symccl sign)) [ intro_replacing id; Tacticals.New.tclTHENLIST [ intros; symmetry; apply (mkVar id); assumption ] ] @@ -4804,6 +4818,8 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make () (* This is probably not very useful any longer *) let prove_transitivity hdcncl eq_kind t = Proofview.Goal.enter { enter = begin fun gl -> + let t = EConstr.of_constr t in + let open EConstr in let (eq1,eq2) = match eq_kind with | MonomorphicLeibnizEq (c1,c2) -> mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |]) @@ -4813,10 +4829,13 @@ let prove_transitivity hdcncl eq_kind t = let env = Proofview.Goal.env gl in let sigma = Tacmach.New.project gl in let type_of = Typing.unsafe_type_of env sigma in - let typt = type_of (EConstr.of_constr t) in + let typt = type_of t in + let typt = EConstr.of_constr typt in (mkApp(hdcncl, [| typ1; c1; typt ;t |]), mkApp(hdcncl, [| typt; t; typ2; c2 |])) in + let eq1 = EConstr.Unsafe.to_constr eq1 in + let eq2 = EConstr.Unsafe.to_constr eq2 in Tacticals.New.tclTHENFIRST (cut eq2) (Tacticals.New.tclTHENFIRST (cut eq1) (Tacticals.New.tclTHENLIST @@ -4830,8 +4849,9 @@ let transitivity_red allowred t = (* PL: usual transitivity don't perform any reduction when searching for an equality, but we may need to do some when called back from inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *) + let sigma = Tacmach.New.project gl in let concl = maybe_betadeltaiota_concl allowred gl in - match_with_equation concl >>= fun with_eqn -> + match_with_equation sigma (EConstr.of_constr concl) >>= fun with_eqn -> match with_eqn with | Some eq_data,_,_ -> Tacticals.New.tclTHEN diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 268453152..368a1df76 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -413,7 +413,7 @@ val subst_one : val declare_intro_decomp_eq : ((int -> unit Proofview.tactic) -> Coqlib.coq_eq_data * types * - (types * constr * constr) -> + (EConstr.types * EConstr.constr * EConstr.constr) -> constr * types -> unit Proofview.tactic) -> unit (** {6 Simple form of basic tactics. } *) |