aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml40
-rw-r--r--pretyping/constr_matching.ml3
-rw-r--r--pretyping/find_subterm.ml3
-rw-r--r--pretyping/glob_ops.ml4
-rw-r--r--pretyping/indrec.ml2
-rw-r--r--pretyping/patternops.ml4
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/recordops.ml2
-rw-r--r--pretyping/unification.ml2
-rw-r--r--pretyping/univdecls.ml7
10 files changed, 43 insertions, 36 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 3a2eac7e79..95de969260 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -208,25 +208,32 @@ and reify_value = function (* reduction under binders *)
| STACK (n,v,stk) ->
lift n (reify_stack (reify_value v) stk)
| CBN(t,env) ->
- t
- (* map_constr_with_binders subs_lift (cbv_norm_term) env t *)
- | LAM (n,ctxt,b,env) ->
- List.fold_left (fun c (n,t) -> mkLambda (n, t, c)) b ctxt
+ apply_env env t
+ | LAM (k,ctxt,b,env) ->
+ apply_env env @@
+ List.fold_left (fun c (n,t) ->
+ mkLambda (n, t, c)) b ctxt
| FIXP ((lij,(names,lty,bds)),env,args) ->
- mkApp
- (mkFix (lij,
- (names,
- lty,
- bds)),
- Array.map reify_value args)
+ let fix = mkFix (lij, (names, lty, bds)) in
+ mkApp (apply_env env fix, Array.map reify_value args)
| COFIXP ((j,(names,lty,bds)),env,args) ->
- mkApp
- (mkCoFix (j,
- (names,lty,bds)),
- Array.map reify_value args)
+ let cofix = mkCoFix (j, (names,lty,bds)) in
+ mkApp (apply_env env cofix, Array.map reify_value args)
| CONSTR (c,args) ->
mkApp(mkConstructU c, Array.map reify_value args)
+and apply_env env t =
+ match kind t with
+ | Rel i ->
+ begin match expand_rel i env with
+ | Inl (k, v) ->
+ reify_value (shift_value k v)
+ | Inr (k,_) ->
+ mkRel k
+ end
+ | _ ->
+ map_with_binders subs_lift apply_env env t
+
(* The main recursive functions
*
* Go under applications and cases/projections (pushed in the stack),
@@ -290,7 +297,10 @@ let rec norm_head info env t stack =
| Evar ev ->
(match evar_value info.infos.i_cache ev with
Some c -> norm_head info env c stack
- | None -> (VAL(0, t), stack))
+ | None ->
+ let e, xs = ev in
+ let xs' = Array.map (apply_env env) xs in
+ (VAL(0, mkEvar (e,xs')), stack))
(* non-neutral cases *)
| Lambda _ ->
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index b7b76c8309..3a91798138 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -12,7 +12,6 @@ open CErrors
open Util
open Names
open Globnames
-open Nameops
open Termops
open Reductionops
open Term
@@ -55,7 +54,7 @@ exception PatternMatchingFailure
let warn_meta_collision =
CWarnings.create ~name:"meta-collision" ~category:"ltac"
(fun name ->
- strbrk "Collision between bound variable " ++ pr_id name ++
+ strbrk "Collision between bound variable " ++ Id.print name ++
strbrk " and a metavariable of same name.")
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 9e7652da64..fd6bfe0a2c 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -12,7 +12,6 @@ open CErrors
open Names
open Locus
open EConstr
-open Nameops
open Termops
open Pretype_errors
@@ -30,7 +29,7 @@ let explain_invalid_occurrence l =
++ prlist_with_sep spc int l ++ str "."
let explain_incorrect_in_value_occurrence id =
- pr_id id ++ str " has no value."
+ Id.print id ++ str " has no value."
let explain_occurrence_error = function
| InvalidOccurrence l -> explain_invalid_occurrence l
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 055fd68f6c..093f1f0b68 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -290,7 +290,7 @@ let warn_variable_collision =
let open Pp in
CWarnings.create ~name:"variable-collision" ~category:"ltac"
(fun name ->
- strbrk "Collision between bound variables of name " ++ pr_id name)
+ strbrk "Collision between bound variables of name " ++ Id.print name)
let add_and_check_ident id set =
if Id.Set.mem id set then warn_variable_collision id;
@@ -524,7 +524,7 @@ let ltac_interp_name { ltac_idents ; ltac_genargs } = function
try Name (Id.Map.find id ltac_idents)
with Not_found ->
if Id.Map.mem id ltac_genargs then
- user_err (str"Ltac variable"++spc()++ pr_id id ++
+ user_err (str"Ltac variable"++spc()++ Id.print id ++
spc()++str"is not bound to an identifier."++spc()++
str"It cannot be used in a binder.")
else n
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml
index 48b33e708c..b7b5b1662a 100644
--- a/pretyping/indrec.ml
+++ b/pretyping/indrec.ml
@@ -616,7 +616,7 @@ let lookup_eliminator ind_sp s =
with Not_found ->
user_err ~hdr:"default_elim"
(strbrk "Cannot find the elimination combinator " ++
- pr_id id ++ strbrk ", the elimination of the inductive definition " ++
+ Id.print id ++ strbrk ", the elimination of the inductive definition " ++
pr_global_env Id.Set.empty (IndRef ind_sp) ++
strbrk " on sort " ++ Termops.pr_sort_family s ++
strbrk " is probably not allowed.")
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index ee79b54744..4d8c09c50a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -230,8 +230,8 @@ let error_instantiate_pattern id l =
| [_] -> "is"
| _ -> "are"
in
- user_err (str "Cannot substitute the term bound to " ++ pr_id id
- ++ strbrk " in pattern because the term refers to " ++ pr_enum pr_id l
+ user_err (str "Cannot substitute the term bound to " ++ Id.print id
+ ++ strbrk " in pattern because the term refers to " ++ pr_enum Id.print l
++ strbrk " which " ++ str is ++ strbrk " not bound in the pattern.")
let instantiate_pattern env sigma lvar c =
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index b2b583ba74..e3470b0f11 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -382,9 +382,9 @@ let check_instance loc subst = function
| [] -> ()
| (id,_) :: _ ->
if List.mem_assoc id subst then
- user_err ?loc (pr_id id ++ str "appears more than once.")
+ user_err ?loc (Id.print id ++ str "appears more than once.")
else
- user_err ?loc (str "No such variable in the signature of the existential variable: " ++ pr_id id ++ str ".")
+ user_err ?loc (str "No such variable in the signature of the existential variable: " ++ Id.print id ++ str ".")
(* used to enforce a name in Lambda when the type constraints itself
is named, hence possibly dependent *)
@@ -410,8 +410,8 @@ let invert_ltac_bound_name lvar env id0 id =
let id' = Id.Map.find id lvar.ltac_idents in
try mkRel (pi1 (lookup_rel_id id' (rel_context env)))
with Not_found ->
- user_err (str "Ltac variable " ++ pr_id id0 ++
- str " depends on pattern variable name " ++ pr_id id ++
+ user_err (str "Ltac variable " ++ Id.print id0 ++
+ str " depends on pattern variable name " ++ Id.print id ++
str " which is not bound in current context.")
let protected_get_type_of env sigma c =
@@ -454,7 +454,7 @@ let pretype_id pretype k0 loc env evdref lvar id =
if Id.Map.mem id lvar.ltac_genargs then begin
let Geninterp.Val.Dyn (typ, _) = Id.Map.find id lvar.ltac_genargs in
user_err ?loc
- (str "Variable " ++ pr_id id ++ str " should be bound to a term but is \
+ (str "Variable " ++ Id.print id ++ str " should be bound to a term but is \
bound to a " ++ Geninterp.Val.pr typ ++ str ".")
end;
(* Check if [id] is a section or goal variable *)
@@ -1089,7 +1089,7 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
with Not_found ->
user_err ?loc (str "Cannot interpret " ++
pr_existential_key !evdref evk ++
- str " in current context: no binding for " ++ pr_id id ++ str ".") in
+ str " in current context: no binding for " ++ Id.print id ++ str ".") in
((id,c)::subst, update) in
let subst,inst = List.fold_right f hyps ([],update) in
check_instance loc subst inst;
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index cb24ca804d..e6d8a0af26 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -300,7 +300,7 @@ let add_canonical_structure x = Lib.add_anonymous_leaf (inCanonStruc x)
let error_not_structure ref =
user_err ~hdr:"object_declare"
- (Nameops.pr_id (basename_of_global ref) ++ str" is not a structure object.")
+ (Id.print (basename_of_global ref) ++ str" is not a structure object.")
let check_and_decompose_canonical_structure ref =
let sp = match ref with ConstRef sp -> sp | _ -> error_not_structure ref in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 5eb6b780ad..a4e2f90d4c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1628,7 +1628,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
if name == Anonymous then next_ident_away_in_goal x ids else
if mem_named_context_val x (named_context_val env) then
user_err ~hdr:"Unification.make_abstraction_core"
- (str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
+ (str "The variable " ++ Id.print x ++ str " is already declared.")
else
x
in
diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index d7c42d03af..5576e33f46 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -6,10 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Names
-open Nameops
-open CErrors
open Pp
+open CErrors
+open Names
(** Local universes and constraints declarations *)
type universe_decl =
@@ -34,7 +33,7 @@ let interp_univ_constraints env evd cstrs =
| GType (Some (loc, Name id)) ->
try loc, Evd.universe_of_name evd (Id.to_string id)
with Not_found ->
- user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ pr_id id)
+ user_err ?loc ~hdr:"interp_constraint" (str "Undeclared universe " ++ Id.print id)
in
let interp (evd,cstrs) (u, d, u') =
let lloc, ul = u_of_id u and rloc, u'l = u_of_id u' in
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 09:46:47 +0000