diff options
| -rw-r--r-- | API/API.mli | 2 | ||||
| -rw-r--r-- | pretyping/constr_matching.ml | 26 | ||||
| -rw-r--r-- | pretyping/constr_matching.mli | 11 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 5 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 8 |
5 files changed, 7 insertions, 45 deletions
diff --git a/API/API.mli b/API/API.mli index 6227f17c6..9a671b43b 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4964,8 +4964,6 @@ sig val pf_conv_x : Goal.goal Evd.sigma -> EConstr.constr -> EConstr.constr -> bool - val pf_is_matching : Goal.goal Evd.sigma -> Pattern.constr_pattern -> EConstr.constr -> bool - val pf_hyps_types : Goal.goal Evd.sigma -> (Names.Id.t * EConstr.types) list val pr_gls : Goal.goal Evd.sigma -> Pp.t diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml index 20ef65c88..478ba73fd 100644 --- a/pretyping/constr_matching.ml +++ b/pretyping/constr_matching.ml @@ -13,7 +13,6 @@ open Util open Names open Globnames open Termops -open Reductionops open Term open EConstr open Vars @@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst = in constrain sigma n c subst -let matches_core env sigma convert allow_partial_app allow_bound_rels +let matches_core env sigma allow_partial_app allow_bound_rels (binding_vars,pat) c = let open EConstr in let convref ref c = @@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels | ConstRef c, Const (c',_) -> Constant.equal c c' | IndRef i, Ind (i', _) -> Names.eq_ind i i' | ConstructRef c, Construct (c',u) -> Names.eq_constructor c c' - | _, _ -> - (if convert then - let sigma,c' = Evd.fresh_global env sigma ref in - is_conv env sigma (EConstr.of_constr c') c - else false) + | _, _ -> false in let rec sorec ctx env subst p t = let cT = strip_outer_cast sigma t in @@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels in sorec [] env (Id.Map.empty, Id.Map.empty) pat c -let matches_core_closed env sigma convert allow_partial_app pat c = - let names, subst = matches_core env sigma convert allow_partial_app false pat c in +let matches_core_closed env sigma allow_partial_app pat c = + let names, subst = matches_core env sigma allow_partial_app false pat c in (names, Id.Map.map snd subst) -let extended_matches env sigma = matches_core env sigma false true true +let extended_matches env sigma = matches_core env sigma true true let matches env sigma pat c = - snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c) + snd (matches_core_closed env sigma true (Id.Set.empty,pat) c) let special_meta = (-1) @@ -412,7 +407,7 @@ let matches_head env sigma pat c = (* Tells if it is an authorized occurrence and if the instance is closed *) let authorized_occ env sigma partial_app closed pat c mk_ctx = try - let subst = matches_core_closed env sigma false partial_app pat c in + let subst = matches_core_closed env sigma partial_app pat c in if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst) then (fun next -> next ()) else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next) @@ -552,10 +547,3 @@ let is_matching_appsubterm ?(closed=true) env sigma pat c = let pat = (Id.Set.empty,pat) in let results = sub_match ~partial_app:true ~closed env sigma pat c in not (IStream.is_empty results) - -let matches_conv env sigma p c = - snd (matches_core_closed env sigma true false (Id.Set.empty,p) c) - -let is_matching_conv env sigma pat n = - try let _ = matches_conv env sigma pat n in true - with PatternMatchingFailure -> false diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli index 780ccc23d..60e1c34a1 100644 --- a/pretyping/constr_matching.mli +++ b/pretyping/constr_matching.mli @@ -55,12 +55,6 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool prefix of it matches against [pat] *) val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool -(** [matches_conv env sigma] matches up to conversion in environment - [(env,sigma)] when constants in pattern are concerned; it raises - [PatternMatchingFailure] if not matchable; bindings are given in - increasing order based on the numbers given in the pattern *) -val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map - (** The type of subterm matching results: a substitution + a context (whose hole is denoted here with [special_meta]) *) type matching_result = @@ -85,8 +79,3 @@ val match_subterm_gen : env -> Evd.evar_map -> (** [is_matching_appsubterm pat c] tells if a subterm of [c] matches against [pat] taking partial subterms into consideration *) val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool - -(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat] - up to conversion for constants in patterns *) -val is_matching_conv : - env -> Evd.evar_map -> constr_pattern -> constr -> bool diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index a8ec4d8ca..cab8d7b52 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,9 +102,6 @@ let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind let pf_hnf_type_of gls = pf_get_type_of gls %> pf_whd_all gls -let pf_is_matching gl p c = pf_apply Constr_matching.is_matching_conv gl p c -let pf_matches gl p c = pf_apply Constr_matching.matches_conv gl p c - (********************************************) (* Definition of the most primitive tactics *) (********************************************) @@ -223,8 +220,6 @@ module New = struct let pf_hnf_type_of gl t = pf_whd_all gl (pf_get_type_of gl t) - let pf_matches gl pat t = pf_apply Constr_matching.matches_conv gl pat t - let pf_whd_all gl t = pf_apply whd_all gl t let pf_compute gl t = pf_apply compute gl t diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index d9496d2b4..e0fb8fbc5 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -12,9 +12,7 @@ open Environ open EConstr open Proof_type open Redexpr -open Pattern open Locus -open Ltac_pretype (** Operations for handling terms under a local typing context. *) @@ -79,10 +77,6 @@ val pf_const_value : goal sigma -> pconstant -> constr val pf_conv_x : goal sigma -> constr -> constr -> bool val pf_conv_x_leq : goal sigma -> constr -> constr -> bool -val pf_matches : goal sigma -> constr_pattern -> constr -> patvar_map -val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool - - (** {6 The most primitive tactics. } *) val refiner : rule -> tactic @@ -138,8 +132,6 @@ module New : sig val pf_whd_all : 'a Proofview.Goal.t -> constr -> constr val pf_compute : 'a Proofview.Goal.t -> constr -> constr - val pf_matches : 'a Proofview.Goal.t -> constr_pattern -> constr -> patvar_map - val pf_nf_evar : 'a Proofview.Goal.t -> constr -> constr end |