aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-07 11:10:43 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-09 11:45:03 +0100
commit59cd53f187939ad32c268cc8ec995d58cee4c297 (patch)
tree549a234c42489ef5641498a02d188f35e8df1d3f
parent37cf90492cb6ed468e696fa052192f1a9fc4b003 (diff)
Remove up-to-conversion matching functions.
They were not used anymore since the previous patches.
-rw-r--r--API/API.mli2
-rw-r--r--pretyping/constr_matching.ml26
-rw-r--r--pretyping/constr_matching.mli11
-rw-r--r--proofs/tacmach.ml5
-rw-r--r--proofs/tacmach.mli8
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