aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml8
-rw-r--r--pretyping/cbv.ml10
-rw-r--r--pretyping/detyping.ml4
-rw-r--r--pretyping/evarutil.ml2
-rw-r--r--pretyping/matching.ml18
-rw-r--r--pretyping/matching.mli15
-rw-r--r--pretyping/pattern.ml20
-rw-r--r--pretyping/pattern.mli19
-rw-r--r--pretyping/pretyping.ml16
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/rawterm.ml22
-rw-r--r--pretyping/rawterm.mli12
-rw-r--r--pretyping/reductionops.ml2
-rw-r--r--pretyping/reductionops.mli6
-rw-r--r--pretyping/retyping.ml2
-rw-r--r--pretyping/retyping.mli4
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/termops.ml16
-rw-r--r--pretyping/termops.mli5
19 files changed, 114 insertions, 71 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index bd38d5c86..c24748970 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -261,7 +261,7 @@ type tomatch_status =
type tomatch_stack = tomatch_status list
-(* Warning: PrLetIn takes a parallel substitution as argument *)
+(* Warning: PrLetIn takes a parallel bindings as argument *)
type predicate_signature =
| PrLetIn of (constr list * constr option) * predicate_signature
@@ -600,7 +600,7 @@ let occur_rawconstr id =
(array_exists occur tyl) or
(not (array_exists (fun id2 -> id=id2) idl) & array_exists occur bv)
| RCast (loc,c,t) -> (occur c) or (occur t)
- | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) -> false
+ | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) -> false
and occur_pattern (loc,idl,p,c) = not (List.mem id idl) & (occur c)
@@ -1025,7 +1025,7 @@ let regeneralize_index_predicate n = map_predicate (regeneralize_index n) 0
let substnl_predicate sigma = map_predicate (substnl sigma)
-(* This is parallel substitution *)
+(* This is parallel bindings *)
let subst_predicate (args,copt) pred =
let sigma = match copt with
| None -> List.rev args
@@ -1144,7 +1144,7 @@ let specialize_predicate tomatchs deps cs = function
let argsi = Array.to_list cs.cs_concl_realargs in
let copti = option_app (fun _ -> build_dependent_constructor cs) copt in
(* The substituends argsi, copti are all defined in gamma, x1...xn *)
- (* We *need _parallel_ substitution to get gamma, x1...xn |- pred'' *)
+ (* We *need _parallel_ bindings to get gamma, x1...xn |- pred'' *)
let pred'' = subst_predicate (argsi, copti) pred' in
(* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *)
let pred''' = liftn_predicate n (n+1) pred'' in
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2599e2958..58d461e57 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -27,12 +27,12 @@ open Esubst
* in normal form and neutral (i.e. not a lambda, a construct or a
* (co)fix, because they may produce redexes by applying them,
* or putting them in a case)
- * LAM(x,a,b,S) is the term [S]([x:a]b). the substitution is propagated
+ * LAM(x,a,b,S) is the term [S]([x:a]b). the bindings is propagated
* only when the abstraction is applied, and then we use the rule
* ([S]([x:a]b) c) --> [S.c]b
* This corresponds to the usual strategy of weak reduction
* FIXP(op,bd,S,args) is the fixpoint (Fix or Cofix) of bodies bd under
- * the substitution S, and then applied to args. Here again,
+ * the bindings S, and then applied to args. Here again,
* weak reduction.
* CONSTR(c,args) is the constructor [c] applied to [args].
*
@@ -67,8 +67,8 @@ let rec shift_value n = function
CONSTR (c, List.map (shift_value n) args)
-(* Contracts a fixpoint: given a fixpoint and a substitution,
- * returns the corresponding fixpoint body, and the substitution in which
+(* Contracts a fixpoint: given a fixpoint and a bindings,
+ * returns the corresponding fixpoint body, and the bindings in which
* it should be evaluated: its first variables are the fixpoint bodies
* (S, (fix Fi {F0 := T0 .. Fn-1 := Tn-1}))
* -> (S. [S]F0 . [S]F1 ... . [S]Fn-1, Ti)
@@ -204,7 +204,7 @@ let rec norm_head info env t stack =
| LetIn (x, b, t, c) ->
(* zeta means letin are contracted; delta without zeta means we *)
- (* allow substitution but leave let's in place *)
+ (* allow bindings but leave let's in place *)
let zeta = red_set (info_flags info) fZETA in
let env' =
if zeta
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b4af4821d..b9751dbc7 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -204,7 +204,9 @@ let rec detype tenv avoid env t =
with Not_found ->
let s = "_UNBOUND_REL_"^(string_of_int n)
in RVar (dummy_loc, id_of_string s))
- | Meta n -> RMeta (dummy_loc, n)
+ | Meta n ->
+ (* Meta in constr are not user-parsable and are mapped to Evar *)
+ REvar (dummy_loc, n)
| Var id ->
(try
let _ = Global.lookup_named id in RRef (dummy_loc, VarRef id)
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 9d65430ed..13ed8e8f6 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -366,7 +366,7 @@ let evar_define isevars (ev,argsv) rhs =
then error_occur_check empty_env (evars_of isevars) ev rhs;
let args = Array.to_list argsv in
let evd = ise_map isevars ev in
- (* the substitution to invert *)
+ (* the bindings to invert *)
let worklist = make_subst (evar_env evd) args in
let body = real_clean isevars ev worklist rhs in
ise_define isevars ev body;
diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index caecbf455..b42365679 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -45,7 +45,7 @@ open Pattern
exception PatternMatchingFailure
-let constrain ((n : int),(m : constr)) sigma =
+let constrain (n,m) sigma =
if List.mem_assoc n sigma then
if eq_constr m (List.assoc n sigma) then sigma
else raise PatternMatchingFailure
@@ -169,11 +169,13 @@ let authorized_occ nocc mres =
if nocc = 0 then mres
else raise (NextOccurrence nocc)
+let special_meta = (-1)
+
(* Tries to match a subterm of [c] with [pat] *)
let rec sub_match nocc pat c =
match kind_of_term c with
| Cast (c1,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
+ (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
| PatternMatchingFailure ->
let (lm,lc) = try_sub_match nocc pat [c1] in
(lm,mkCast (List.hd lc, c2))
@@ -181,7 +183,7 @@ let rec sub_match nocc pat c =
let (lm,lc) = try_sub_match (nocc - 1) pat [c1] in
(lm,mkCast (List.hd lc, c2)))
| Lambda (x,c1,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
+ (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
| PatternMatchingFailure ->
let (lm,lc) = try_sub_match nocc pat [c1;c2] in
(lm,mkLambda (x,List.hd lc,List.nth lc 1))
@@ -189,7 +191,7 @@ let rec sub_match nocc pat c =
let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
(lm,mkLambda (x,List.hd lc,List.nth lc 1)))
| Prod (x,c1,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
+ (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
| PatternMatchingFailure ->
let (lm,lc) = try_sub_match nocc pat [c1;c2] in
(lm,mkProd (x,List.hd lc,List.nth lc 1))
@@ -197,7 +199,7 @@ let rec sub_match nocc pat c =
let (lm,lc) = try_sub_match (nocc - 1) pat [c1;c2] in
(lm,mkProd (x,List.hd lc,List.nth lc 1)))
| LetIn (x,c1,t2,c2) ->
- (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
+ (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
| PatternMatchingFailure ->
let (lm,lc) = try_sub_match nocc pat [c1;t2;c2] in
(lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2))
@@ -205,7 +207,7 @@ let rec sub_match nocc pat c =
let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
(lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
| App (c1,lc) ->
- (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
+ (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
| PatternMatchingFailure ->
let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
(lm,mkApp (List.hd le, Array.of_list (List.tl le)))
@@ -213,7 +215,7 @@ let rec sub_match nocc pat c =
let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
(lm,mkApp (List.hd le, Array.of_list (List.tl le))))
| Case (ci,hd,c1,lc) ->
- (try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
+ (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
| PatternMatchingFailure ->
let (lm,le) = try_sub_match nocc pat (c1::Array.to_list lc) in
(lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le)))
@@ -222,7 +224,7 @@ let rec sub_match nocc pat c =
(lm,mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))))
| Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
| Rel _|Meta _|Var _|Sort _ ->
- (try authorized_occ nocc ((matches pat c),mkMeta (-1)) with
+ (try authorized_occ nocc ((matches pat c),mkMeta special_meta) with
| PatternMatchingFailure -> raise (NextOccurrence nocc)
| NextOccurrence nocc -> raise (NextOccurrence (nocc - 1)))
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 5a789b442..32c2906b6 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -13,38 +13,37 @@ open Names
open Term
open Environ
open Pattern
+open Termops
(*i*)
(*s This modules implements pattern-matching on terms *)
exception PatternMatchingFailure
+val special_meta : metavariable
+
(* [matches pat c] matches [c] against [pat] and returns the resulting
assignment of metavariables; it raises [PatternMatchingFailure] if
not matchable; bindings are given in increasing order based on the
numbers given in the pattern *)
-val matches :
- constr_pattern -> constr -> (int * constr) list
+val matches : constr_pattern -> constr -> patvar_map
(* [is_matching pat c] just tells if [c] matches against [pat] *)
-val is_matching :
- constr_pattern -> constr -> bool
+val is_matching : 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 -> (int * constr) list
+val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
(* To skip to the next occurrence *)
exception NextOccurrence of int
(* Tries to match a subterm of [c] with [pat] *)
-val sub_match :
- int -> constr_pattern -> constr -> ((int * constr) list * constr)
+val sub_match : int -> constr_pattern -> constr -> patvar_map * constr
(* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
up to conversion for constants in patterns *)
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 9dafda587..5ad06a6e5 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -18,18 +18,26 @@ open Environ
open Nametab
open Pp
+(* Metavariables *)
+
+type patvar_map = (patvar * constr) list
+let patvar_of_int n = Names.id_of_string (string_of_int n)
+let pr_patvar = pr_id
+
+(* Patterns *)
+
type constr_pattern =
| PRef of global_reference
| PVar of identifier
| PEvar of existential_key
| PRel of int
| PApp of constr_pattern * constr_pattern array
- | PSoApp of int * constr_pattern list
+ | PSoApp of patvar * constr_pattern list
| PLambda of name * constr_pattern * constr_pattern
| PProd of name * constr_pattern * constr_pattern
| PLetIn of name * constr_pattern * constr_pattern
| PSort of rawsort
- | PMeta of int option
+ | PMeta of patvar option
| PCase of case_style * constr_pattern option * constr_pattern *
constr_pattern array
| PFix of fixpoint
@@ -151,7 +159,7 @@ let head_of_constr_reference c = match kind_of_term c with
let rec pattern_of_constr t =
match kind_of_term t with
| Rel n -> PRel n
- | Meta n -> PMeta (Some n)
+ | Meta n -> PMeta (Some (id_of_string (string_of_int n)))
| Var id -> PVar id
| Sort (Prop c) -> PSort (RProp c)
| Sort (Type _) -> PSort (RType None)
@@ -197,13 +205,13 @@ let rec pat_of_raw metas vars = function
| RVar (_,id) ->
(try PRel (list_index (Name id) vars)
with Not_found -> PVar id)
- | RMeta (_,n) ->
+ | RPatVar (_,(false,n)) ->
metas := n::!metas; PMeta (Some n)
| RRef (_,r) ->
PRef r
(* Hack pour ne pas réécrire une interprétation complète des patterns*)
- | RApp (_, RMeta (_,n), cl) when n<0 ->
- PSoApp (- n, List.map (pat_of_raw metas vars) cl)
+ | RApp (_, RPatVar (_,(true,n)), cl) ->
+ PSoApp (n, List.map (pat_of_raw metas vars) cl)
| RApp (_,c,cl) ->
PApp (pat_of_raw metas vars c,
Array.of_list (List.map (pat_of_raw metas vars) cl))
diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli
index 11821a6a8..535ca8c01 100644
--- a/pretyping/pattern.mli
+++ b/pretyping/pattern.mli
@@ -9,26 +9,36 @@
(*i $Id$ i*)
(*i*)
+open Pp
open Names
open Sign
open Term
open Environ
open Libnames
open Nametab
+open Rawterm
(*i*)
+(* Pattern variables *)
+
+type patvar_map = (patvar * constr) list
+val patvar_of_int : int -> patvar
+val pr_patvar : patvar -> std_ppcmds
+
+(* Patterns *)
+
type constr_pattern =
| PRef of global_reference
| PVar of identifier
| PEvar of existential_key
| PRel of int
| PApp of constr_pattern * constr_pattern array
- | PSoApp of int * constr_pattern list
+ | PSoApp of patvar * constr_pattern list
| PLambda of name * constr_pattern * constr_pattern
| PProd of name * constr_pattern * constr_pattern
| PLetIn of name * constr_pattern * constr_pattern
- | PSort of Rawterm.rawsort
- | PMeta of int option
+ | PSort of rawsort
+ | PMeta of patvar option
| PCase of case_style * constr_pattern option * constr_pattern *
constr_pattern array
| PFix of fixpoint
@@ -71,7 +81,8 @@ val pattern_of_constr : constr -> constr_pattern
a pattern; variables bound in [l] are replaced by the pattern to which they
are bound *)
-val pattern_of_rawconstr : Rawterm.rawconstr -> int list * constr_pattern
+val pattern_of_rawconstr : rawconstr ->
+ patvar list * constr_pattern
val instantiate_pattern :
(identifier * constr_pattern) list -> constr_pattern -> constr_pattern
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e4714468a..f94c14e71 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -28,6 +28,7 @@ open Pretype_errors
open Rawterm
open Evarconv
open Coercion
+open Pattern
open Dyn
@@ -151,7 +152,13 @@ let evar_type_case isevars env ct pt lft p c =
in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
*)
-let pretype_id loc env lvar id =
+let strip_meta id = (* For Grammar v7 compatibility *)
+ let s = string_of_id id in
+ if s.[0]='$' then id_of_string (String.sub s 1 (String.length s - 1))
+ else id
+
+let pretype_id loc env lvar id =
+ let id = strip_meta id in (* May happen in tactics defined by Grammar *)
try
List.assoc id lvar
with Not_found ->
@@ -217,7 +224,8 @@ let rec pretype tycon env isevars lvar lmeta = function
let j = (Retyping.get_judgment_of env (evars_of isevars) c) in
inh_conv_coerce_to_tycon loc env isevars j tycon
- | RMeta (loc,n) ->
+ | RPatVar (loc,(someta,n)) ->
+ assert (not someta);
let j =
try
List.assoc n lmeta
@@ -225,7 +233,7 @@ let rec pretype tycon env isevars lvar lmeta = function
Not_found ->
user_err_loc
(loc,"pretype",
- str "Metavariable " ++ int n ++ str " is unbound")
+ str "Metavariable " ++ pr_patvar n ++ str " is unbound")
in inh_conv_coerce_to_tycon loc env isevars j tycon
| RHole (loc,k) ->
@@ -618,7 +626,7 @@ let ise_infer_type_gen fail_evar sigma env lvar lmeta c =
check_evars fail_evar env sigma isevars tj.utj_val;
(evars_of isevars, tj)
-type meta_map = (int * unsafe_judgment) list
+type meta_map = (patvar * unsafe_judgment) list
type var_map = (identifier * unsafe_judgment) list
let understand_judgment sigma env c =
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index dadc8b94c..e6dc58896 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -18,7 +18,7 @@ open Rawterm
open Evarutil
(*i*)
-type meta_map = (int * unsafe_judgment) list
+type meta_map = (patvar * unsafe_judgment) list
type var_map = (identifier * unsafe_judgment) list
(* constr with holes *)
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index 0dcf90188..3e13cd861 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -31,6 +31,8 @@ let pattern_loc = function
PatVar(loc,_) -> loc
| PatCstr(loc,_,_,_) -> loc
+type patvar = identifier
+
type rawsort = RProp of Term.contents | RType of Univ.universe option
type fix_kind = RFix of (int array * int) | RCoFix of int
@@ -39,14 +41,14 @@ type binder_kind = BProd | BLambda | BLetIn
type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
-type 'a explicit_substitution = (loc * quantified_hypothesis * 'a) list
+type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
-type 'a substitution =
+type 'a bindings =
| ImplicitBindings of 'a list
- | ExplicitBindings of 'a explicit_substitution
+ | ExplicitBindings of 'a explicit_bindings
| NoBindings
-type 'a with_bindings = 'a * 'a substitution
+type 'a with_bindings = 'a * 'a bindings
type hole_kind =
| ImplicitArg of global_reference * int
@@ -60,7 +62,7 @@ type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
| REvar of loc * existential_key
- | RMeta of loc * int
+ | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
| RApp of loc * rawconstr * rawconstr list
| RLambda of loc * name * rawconstr * rawconstr
| RProd of loc * name * rawconstr * rawconstr
@@ -101,7 +103,7 @@ let loc = function
| RHole (loc,_) -> loc
| RRef (loc,_) -> loc
| REvar (loc,_) -> loc
- | RMeta (loc,_) -> loc
+ | RPatVar (loc,_) -> loc
| RDynamic (loc,_) -> loc
let map_rawconstr f = function
@@ -117,7 +119,7 @@ let map_rawconstr f = function
ROrderedCase (loc,b,option_app f tyopt,f tm, Array.map f bv)
| RRec (loc,fk,idl,tyl,bv) -> RRec (loc,fk,idl,Array.map f tyl,Array.map f bv)
| RCast (loc,c,t) -> RCast (loc,f c,f t)
- | (RSort _ | RHole _ | RRef _ | REvar _ | RMeta _ | RDynamic _) as x -> x
+ | (RSort _ | RHole _ | RRef _ | REvar _ | RPatVar _ | RDynamic _) as x -> x
(*
let name_app f e = function
@@ -155,7 +157,7 @@ let map_rawconstr_with_binders_loc loc g f e = function
| RHole (_,x) -> RHole (loc,x)
| RRef (_,x) -> RRef (loc,x)
| REvar (_,x) -> REvar (loc,x)
- | RMeta (_,x) -> RMeta (loc,x)
+ | RPatVar (_,x) -> RPatVar (loc,x)
| RDynamic (_,x) -> RDynamic (loc,x)
*)
@@ -177,7 +179,7 @@ let rec subst_raw subst raw =
| RVar _ -> raw
| REvar _ -> raw
- | RMeta _ -> raw
+ | RPatVar _ -> raw
| RApp (loc,r,rl) ->
let r' = subst_raw subst r
@@ -247,7 +249,7 @@ let loc_of_rawconstr = function
| RRef (loc,_) -> loc
| RVar (loc,_) -> loc
| REvar (loc,_) -> loc
- | RMeta (loc,_) -> loc
+ | RPatVar (loc,_) -> loc
| RApp (loc,_,_) -> loc
| RLambda (loc,_,_,_) -> loc
| RProd (loc,_,_,_) -> loc
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 293667aed..fbd01db9a 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -29,6 +29,8 @@ type cases_pattern =
val pattern_loc : cases_pattern -> loc
+type patvar = identifier
+
type rawsort = RProp of Term.contents | RType of Univ.universe option
type fix_kind = RFix of (int array * int) | RCoFix of int
@@ -37,14 +39,14 @@ type binder_kind = BProd | BLambda | BLetIn
type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier
-type 'a explicit_substitution = (loc * quantified_hypothesis * 'a) list
+type 'a explicit_bindings = (loc * quantified_hypothesis * 'a) list
-type 'a substitution =
+type 'a bindings =
| ImplicitBindings of 'a list
- | ExplicitBindings of 'a explicit_substitution
+ | ExplicitBindings of 'a explicit_bindings
| NoBindings
-type 'a with_bindings = 'a * 'a substitution
+type 'a with_bindings = 'a * 'a bindings
type hole_kind =
| ImplicitArg of global_reference * int
@@ -58,7 +60,7 @@ type rawconstr =
| RRef of (loc * global_reference)
| RVar of (loc * identifier)
| REvar of loc * existential_key
- | RMeta of loc * int
+ | RPatVar of loc * (bool * patvar) (* Used for patterns only *)
| RApp of loc * rawconstr * rawconstr list
| RLambda of loc * name * rawconstr * rawconstr
| RProd of loc * name * rawconstr * rawconstr
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b2d60176d..9b51abff3 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -76,7 +76,7 @@ let rec strong_prodspine redfun c =
| _ -> x
(*************************************)
-(*** Reduction using substitutions ***)
+(*** Reduction using bindingss ***)
(*************************************)
(* This signature is very similar to Closure.RedFlagsSig except there
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 5cf0bfd91..d2f260b7b 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -192,9 +192,9 @@ val is_fconv : conv_pb -> env -> evar_map -> constr -> constr -> bool
(*s Special-Purpose Reduction Functions *)
-val whd_meta : (int * constr) list -> constr -> constr
-val plain_instance : (int * constr) list -> constr -> constr
-val instance : (int * constr) list -> constr -> constr
+val whd_meta : (metavariable * constr) list -> constr -> constr
+val plain_instance : (metavariable * constr) list -> constr -> constr
+val instance : (metavariable * constr) list -> constr -> constr
(*s Obsolete Reduction Functions *)
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index aa5d27d20..43218ca72 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -18,8 +18,6 @@ open Typeops
open Declarations
open Instantiate
-type metamap = (int * constr) list
-
let outsort env sigma t =
match kind_of_term (whd_betadeltaiota env sigma t) with
| Sort s -> s
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index cec8c5f9d..d7c1c516e 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -13,6 +13,8 @@ open Names
open Term
open Evd
open Environ
+open Pattern
+open Termops
(*i*)
(* This family of functions assumes its constr argument is known to be
@@ -21,8 +23,6 @@ open Environ
either produces a wrong result or raise an anomaly. Use with care.
It doesn't handle predicative universes too. *)
-type metamap = (int * constr) list
-
val get_type_of : env -> evar_map -> constr -> constr
val get_sort_of : env -> evar_map -> types -> sorts
val get_sort_family_of : env -> evar_map -> types -> sorts_family
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 7dc78cbe6..13fefd306 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -623,7 +623,7 @@ let contextually (locs,c) f env sigma t =
errorlabstrm "contextually" (str "Too few occurences");
t'
-(* linear substitution (following pretty-printer) of the value of name in c.
+(* linear bindings (following pretty-printer) of the value of name in c.
* n is the number of the next occurence of name.
* ol is the occurence list to find. *)
let rec substlin env name n ol c =
diff --git a/pretyping/termops.ml b/pretyping/termops.ml
index a41631bd2..080ed4374 100644
--- a/pretyping/termops.ml
+++ b/pretyping/termops.ml
@@ -18,6 +18,8 @@ open Environ
open Libnames
open Nametab
+(* Sorts and sort family *)
+
let print_sort = function
| Prop Pos -> (str "Set")
| Prop Null -> (str "Prop")
@@ -399,9 +401,11 @@ let dependent m t =
let pop t = lift (-1) t
(***************************)
-(* substitution functions *)
+(* bindings functions *)
(***************************)
+type metamap = (metavariable * constr) list
+
let rec subst_meta bl c =
match kind_of_term c with
| Meta i -> (try List.assoc i bl with Not_found -> c)
@@ -473,7 +477,7 @@ let replace_term = replace_term_gen eq_constr
(* Substitute only a list of locations locs, the empty list is
interpreted as substitute all, if 0 is in the list then no
- substitution is done. The list may contain only negative occurrences
+ bindings is done. The list may contain only negative occurrences
that will not be substituted. *)
let subst_term_occ_gen locs occ c t =
@@ -697,9 +701,15 @@ let occur_id env nenv id0 c =
with Occur -> true
| Not_found -> false (* Case when a global is not in the env *)
+let is_section_variable id =
+ try let _ = Declare.find_section_variable id in true with Not_found -> false
+
let next_name_not_occuring env name l env_names t =
let rec next id =
- if List.mem id l or occur_id env env_names id t then next (lift_ident id)
+ if List.mem id l or occur_id env env_names id t or
+ (* To be consistent with intro mechanism *)
+ (Declare.is_global id & not (is_section_variable id))
+ then next (lift_ident id)
else id
in
match name with
diff --git a/pretyping/termops.mli b/pretyping/termops.mli
index cd5d7def0..216a090c4 100644
--- a/pretyping/termops.mli
+++ b/pretyping/termops.mli
@@ -86,12 +86,13 @@ val occur_term : constr -> constr -> bool
val free_rels : constr -> Intset.t
(* Substitution of metavariables *)
-val subst_meta : (int * constr) list -> constr -> constr
+type metamap = (metavariable * constr) list
+val subst_meta : metamap -> constr -> constr
(* [pop c] lifts by -1 the positive indexes in [c] *)
val pop : constr -> constr
-(* substitution of an arbitrary large term. Uses equality modulo
+(* bindings of an arbitrary large term. Uses equality modulo
reduction of let *)
val dependent : constr -> constr -> bool
val subst_term_gen :
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 02:11:29 +0000