aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/using/tools/coqdoc.rst2
-rw-r--r--engine/eConstr.ml5
-rw-r--r--engine/eConstr.mli3
-rw-r--r--engine/evarutil.ml22
-rw-r--r--engine/evarutil.mli2
-rw-r--r--engine/univSubst.ml6
-rw-r--r--kernel/cbytegen.ml20
-rw-r--r--kernel/environ.mli2
-rw-r--r--pretyping/globEnv.ml24
-rw-r--r--theories/Program/Equality.v2
-rw-r--r--vernac/comInductive.ml29
11 files changed, 71 insertions, 46 deletions
diff --git a/doc/sphinx/using/tools/coqdoc.rst b/doc/sphinx/using/tools/coqdoc.rst
index f872c1b2e3..9ac3d2adda 100644
--- a/doc/sphinx/using/tools/coqdoc.rst
+++ b/doc/sphinx/using/tools/coqdoc.rst
@@ -1,3 +1,5 @@
+.. index:: coqdoc
+
.. _coqdoc:
Documenting |Coq| files with coqdoc
diff --git a/engine/eConstr.ml b/engine/eConstr.ml
index ca681e58f8..42c9359ff0 100644
--- a/engine/eConstr.ml
+++ b/engine/eConstr.ml
@@ -733,6 +733,11 @@ let map_rel_context_in_env f env sign =
in
aux env [] (List.rev sign)
+let match_named_context_val :
+ named_context_val -> (named_declaration * lazy_val * named_context_val) option =
+ match unsafe_eq with
+ | Refl -> match_named_context_val
+
let fresh_global ?loc ?rigid ?names env sigma reference =
let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in
evd, t
diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 9a73c3e3f5..aea441b90b 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -322,6 +322,9 @@ val lookup_named_val : variable -> named_context_val -> named_declaration
val map_rel_context_in_env :
(env -> constr -> constr) -> env -> rel_context -> rel_context
+val match_named_context_val :
+ named_context_val -> (named_declaration * lazy_val * named_context_val) option
+
(* XXX Missing Sigma proxy *)
val fresh_global :
?loc:Loc.t -> ?rigid:Evd.rigid -> ?names:Univ.Instance.t -> Environ.env ->
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 5fcadfcef7..eea7e38f87 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -287,7 +287,7 @@ let csubst_subst { csubst_len = k; csubst_var = v; csubst_rel = s } c =
EConstr.of_constr c
type ext_named_context =
- csubst * Id.Set.t * EConstr.named_context
+ csubst * Id.Set.t * named_context_val
let push_var id { csubst_len = n; csubst_var = v; csubst_rel = s; csubst_rev = r } =
let s = Int.Map.add n (Constr.mkVar id) s in
@@ -325,22 +325,22 @@ type naming_mode =
let push_rel_decl_to_named_context
?(hypnaming=KeepUserNameAndRenameExistingButSectionNames)
- sigma decl (subst, avoid, nc) =
+ sigma decl ((subst, avoid, nc) : ext_named_context) =
let open EConstr in
let open Vars in
let map_decl f d =
NamedDecl.map_constr f d
in
- let rec replace_var_named_declaration id0 id = function
- | [] -> []
- | decl :: nc ->
+ let rec replace_var_named_declaration id0 id nc = match match_named_context_val nc with
+ | None -> empty_named_context_val
+ | Some (decl, _, nc) ->
if Id.equal id0 (NamedDecl.get_id decl) then
(* Stop here, the variable cannot occur before its definition *)
- (NamedDecl.set_id id decl) :: nc
+ push_named_context_val (NamedDecl.set_id id decl) nc
else
let nc = replace_var_named_declaration id0 id nc in
let vsubst = [id0 , mkVar id] in
- map_decl (fun c -> replace_vars vsubst c) decl :: nc
+ push_named_context_val (map_decl (fun c -> replace_vars vsubst c) decl) nc
in
let extract_if_neq id = function
| Anonymous -> None
@@ -372,7 +372,7 @@ let push_rel_decl_to_named_context
let subst = update_var id0 id subst in
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id0) |> map_decl (csubst_subst subst) in
let nc = replace_var_named_declaration id0 id nc in
- (push_var id0 subst, Id.Set.add id avoid, d :: nc)
+ (push_var id0 subst, Id.Set.add id avoid, push_named_context_val d nc)
| Some id0 when hypnaming = FailIfConflict ->
user_err Pp.(Id.print id0 ++ str " is already used.")
| _ ->
@@ -381,7 +381,7 @@ let push_rel_decl_to_named_context
the new binder has name [id]. Which amounts to the same
behaviour than when [id=id0]. *)
let d = decl |> NamedDecl.of_rel_decl (fun _ -> id) |> map_decl (csubst_subst subst) in
- (push_var id subst, Id.Set.add id avoid, d :: nc)
+ (push_var id subst, Id.Set.add id avoid, push_named_context_val d nc)
let push_rel_context_to_named_context ?hypnaming env sigma typ =
(* compute the instances relative to the named context and rel_context *)
@@ -399,8 +399,8 @@ let push_rel_context_to_named_context ?hypnaming env sigma typ =
(* We do keep the instances corresponding to local definition (see above) *)
let (subst, _, env) =
Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ?hypnaming sigma d acc)
- (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
- (val_of_named_context env, csubst_subst subst typ, inst_rels@inst_vars, subst)
+ (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
+ (env, csubst_subst subst typ, inst_rels@inst_vars, subst)
(*------------------------------------*
* Entry points to define new evars *
diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index b5c7ccb283..b3c94e6b3b 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -268,7 +268,7 @@ val empty_csubst : csubst
val csubst_subst : csubst -> constr -> constr
type ext_named_context =
- csubst * Id.Set.t * named_context
+ csubst * Id.Set.t * named_context_val
val push_rel_decl_to_named_context : ?hypnaming:naming_mode ->
evar_map -> rel_declaration -> ext_named_context -> ext_named_context
diff --git a/engine/univSubst.ml b/engine/univSubst.ml
index a691239ee2..92211d5f3d 100644
--- a/engine/univSubst.ml
+++ b/engine/univSubst.ml
@@ -131,9 +131,9 @@ let nf_evars_and_universes_opt_subst f subst =
let rec aux c =
match kind c with
| Evar (evk, args) ->
- let args = List.map aux args in
- (match try f (evk, args) with Not_found -> None with
- | None -> mkEvar (evk, args)
+ let args' = List.Smart.map aux args in
+ (match try f (evk, args') with Not_found -> None with
+ | None -> if args == args' then c else mkEvar (evk, args')
| Some c -> aux c)
| Const pu ->
let pu' = subst_univs_fn_puniverses lsubst pu in
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index b3a4bd7471..59ae8c0745 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -130,7 +130,7 @@ type comp_env = {
nb_uni_stack : int ; (* number of universes on the stack, *)
(* universes are always at the bottom. *)
nb_stack : int; (* number of variables on the stack *)
- in_stack : int list; (* position in the stack *)
+ in_stack : int Range.t; (* position in the stack *)
nb_rec : int; (* number of mutually recursive functions *)
pos_rec : instruction list; (* instruction d'acces pour les variables *)
(* de point fix ou de cofix *)
@@ -158,7 +158,7 @@ let empty_comp_env ()=
{ arity = 0;
nb_uni_stack = 0;
nb_stack = 0;
- in_stack = [];
+ in_stack = Range.empty;
nb_rec = 0;
pos_rec = [];
offset = 0;
@@ -188,13 +188,13 @@ let ensure_stack_capacity f x =
(*i Creation functions for comp_env *)
let rec add_param n sz l =
- if Int.equal n 0 then l else add_param (n - 1) sz (n+sz::l)
+ if Int.equal n 0 then l else add_param (n - 1) sz (Range.cons (n+sz) l)
let comp_env_fun ?(univs=0) arity =
{ arity;
nb_uni_stack = univs ;
nb_stack = arity;
- in_stack = add_param arity 0 [];
+ in_stack = add_param arity 0 Range.empty;
nb_rec = 0;
pos_rec = [];
offset = 1;
@@ -206,7 +206,7 @@ let comp_env_fix_type rfv =
{ arity = 0;
nb_uni_stack = 0;
nb_stack = 0;
- in_stack = [];
+ in_stack = Range.empty;
nb_rec = 0;
pos_rec = [];
offset = 1;
@@ -221,7 +221,7 @@ let comp_env_fix ndef curr_pos arity rfv =
{ arity;
nb_uni_stack = 0;
nb_stack = arity;
- in_stack = add_param arity 0 [];
+ in_stack = add_param arity 0 Range.empty;
nb_rec = ndef;
pos_rec = !prec;
offset = 2 * (ndef - curr_pos - 1)+1;
@@ -232,7 +232,7 @@ let comp_env_cofix_type ndef rfv =
{ arity = 0;
nb_uni_stack = 0;
nb_stack = 0;
- in_stack = [];
+ in_stack = Range.empty;
nb_rec = 0;
pos_rec = [];
offset = 1+ndef;
@@ -247,7 +247,7 @@ let comp_env_cofix ndef arity rfv =
{ arity;
nb_uni_stack = 0;
nb_stack = arity;
- in_stack = add_param arity 0 [];
+ in_stack = add_param arity 0 Range.empty;
nb_rec = ndef;
pos_rec = !prec;
offset = ndef+1;
@@ -264,7 +264,7 @@ let push_param n sz r =
let push_local sz r =
{ r with
nb_stack = r.nb_stack + 1;
- in_stack = (sz + 1) :: r.in_stack }
+ in_stack = Range.cons (sz + 1) r.in_stack }
(*i Compilation of variables *)
let find_at fv env = FvMap.find fv env.fv_fwd
@@ -280,7 +280,7 @@ let pos_named id r =
let pos_rel i r sz =
if i <= r.nb_stack then
- Kacc(sz - (List.nth r.in_stack (i-1)))
+ Kacc(sz - (Range.get r.in_stack (i-1)))
else
let i = i - r.nb_stack in
if i <= r.nb_rec then
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 79e632daa0..f489b13a3b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -176,6 +176,8 @@ val named_body : variable -> env -> constr option
val fold_named_context :
(env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a
+val match_named_context_val : named_context_val -> (named_declaration * lazy_val * named_context_val) option
+
(** Recurrence on [named_context] starting from younger decl *)
val fold_named_context_reverse :
('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index fad41614b4..05abb86f46 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -33,6 +33,8 @@ type t = {
(** For locating indices *)
renamed_env : env;
(** For name management *)
+ renamed_vars : EConstr.t list Lazy.t;
+ (** Identity instance of named_context of renamed_env, to maximize sharing *)
extra : ext_named_context Lazy.t;
(** Delay the computation of the evar extended environment *)
lvar : ltac_var_map;
@@ -42,10 +44,12 @@ let make ~hypnaming env sigma lvar =
let get_extra env sigma =
let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
- (rel_context env) ~init:(empty_csubst, avoid, named_context env) in
+ (rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
+ let open Context.Named.Declaration in
{
static_env = env;
renamed_env = env;
+ renamed_vars = lazy (List.map (get_id %> mkVar) (named_context env));
extra = lazy (get_extra env sigma);
lvar = lvar;
}
@@ -67,10 +71,12 @@ let ltac_interp_id { ltac_idents ; ltac_genargs } id =
let ltac_interp_name lvar = Nameops.Name.map (ltac_interp_id lvar)
let push_rel ~hypnaming sigma d env =
- let d' = Context.Rel.Declaration.map_name (ltac_interp_name env.lvar) d in
+ let open Context.Rel.Declaration in
+ let d' = map_name (ltac_interp_name env.lvar) d in
let env = {
static_env = push_rel d env.static_env;
renamed_env = push_rel d' env.renamed_env;
+ renamed_vars = env.renamed_vars;
extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
lvar = env.lvar;
} in
@@ -83,6 +89,7 @@ let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
let env = {
static_env = push_rel_context ctx env.static_env;
renamed_env = push_rel_context ctx' env.renamed_env;
+ renamed_vars = env.renamed_vars;
extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
lvar = env.lvar;
} in
@@ -95,13 +102,14 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env =
Array.map get_annot ctx, env
let new_evar env sigma ?src ?naming typ =
- let open Context.Named.Declaration in
- let inst_vars = List.map (get_id %> mkVar) (named_context env.renamed_env) in
- let inst_rels = List.rev (rel_list 0 (nb_rel env.renamed_env)) in
- let (subst, _, nc) = Lazy.force env.extra in
+ let lazy inst_vars = env.renamed_vars in
+ let rec rel_list n accu =
+ if n <= 0 then accu
+ else rel_list (n - 1) (mkRel n :: accu)
+ in
+ let instance = rel_list (nb_rel env.renamed_env) inst_vars in
+ let (subst, _, sign) = Lazy.force env.extra in
let typ' = csubst_subst subst typ in
- let instance = inst_rels @ inst_vars in
- let sign = val_of_named_context nc in
new_evar_instance sign sigma typ' ?src ?naming instance
let new_type_evar env sigma ~src =
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index b46ddaa32b..5862a08838 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -264,7 +264,7 @@ Class DependentEliminationPackage (A : Type) :=
Ltac elim_tac tac p :=
let ty := type of p in
- let eliminator := eval simpl in (@elim (_ : DependentEliminationPackage ty)) in
+ let eliminator := eval simpl in (@elim _ (_ : DependentEliminationPackage ty)) in
tac p eliminator.
(** Specialization to do case analysis or induction.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index 95489c9132..e490b33dde 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -60,23 +60,28 @@ type structured_one_inductive_expr = {
ind_lc : (Id.t * constr_expr) list
}
+exception Same of Id.t
+
let check_all_names_different indl =
+ let rec elements = function
+ | [] -> Id.Set.empty
+ | id :: l ->
+ let s = elements l in
+ if Id.Set.mem id s then raise (Same id) else Id.Set.add id s
+ in
let ind_names = List.map (fun ind -> ind.ind_name) indl in
let cstr_names = List.map_append (fun ind -> List.map fst ind.ind_lc) indl in
- let l = List.duplicates Id.equal ind_names in
- let () = match l with
- | [] -> ()
- | t :: _ -> raise (InductiveError (SameNamesTypes t))
+ let ind_names = match elements ind_names with
+ | s -> s
+ | exception (Same t) -> raise (InductiveError (SameNamesTypes t))
in
- let l = List.duplicates Id.equal cstr_names in
- let () = match l with
- | [] -> ()
- | c :: _ -> raise (InductiveError (SameNamesConstructors (List.hd l)))
+ let cstr_names = match elements cstr_names with
+ | s -> s
+ | exception (Same c) -> raise (InductiveError (SameNamesConstructors c))
in
- let l = List.intersect Id.equal ind_names cstr_names in
- match l with
- | [] -> ()
- | _ -> raise (InductiveError (SameNamesOverlap l))
+ let l = Id.Set.inter ind_names cstr_names in
+ if not (Id.Set.is_empty l) then
+ raise (InductiveError (SameNamesOverlap (Id.Set.elements l)))
(** Make the arity conclusion flexible to avoid generating an upper bound universe now,
only if the universe does not appear anywhere else.
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-09 03:02:22 +0000