aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/assumptions.ml2
-rw-r--r--toplevel/assumptions.mli2
-rw-r--r--toplevel/auto_ind_decl.ml7
-rw-r--r--toplevel/class.ml5
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/classes.mli5
-rw-r--r--toplevel/command.ml15
-rw-r--r--toplevel/discharge.ml7
-rw-r--r--toplevel/discharge.mli3
-rw-r--r--toplevel/obligations.ml5
-rw-r--r--toplevel/record.ml11
-rw-r--r--toplevel/record.mli7
-rw-r--r--toplevel/vernacentries.ml2
13 files changed, 32 insertions, 41 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index a71588fe0..470485438 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -141,7 +141,7 @@ let label_of = function
| ConstructRef ((kn,_),_) -> pi3 (repr_mind kn)
| VarRef id -> Label.of_id id
-let push (r : Context.rel_declaration) (ctx : Context.rel_context) = r :: ctx
+let push (r : Context.Rel.Declaration.t) (ctx : Context.Rel.t) = r :: ctx
let rec traverse current ctx accu t = match kind_of_term t with
| Var id ->
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index f89b39543..21039f571 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -21,7 +21,7 @@ open Printer
val traverse :
Label.t -> constr ->
(Refset_env.t * Refset_env.t Refmap_env.t *
- (label * Context.rel_context * types) list Refmap_env.t)
+ (label * Context.Rel.t * types) list Refmap_env.t)
(** Collects all the assumptions (optionally including opaque definitions)
on which a term relies (together with their type). The above warning of
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 98686fb1b..56106928e 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -15,7 +15,6 @@ open Util
open Pp
open Term
open Vars
-open Context
open Termops
open Declarations
open Names
@@ -103,7 +102,7 @@ let mkFullInd (ind,u) n =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
if nparrec > 0
then mkApp (mkIndU (ind,u),
- Array.of_list(extended_rel_list (nparrec+n) lnamesparrec))
+ Array.of_list(Context.Rel.to_extended_list (nparrec+n) lnamesparrec))
else mkIndU (ind,u)
let check_bool_is_defined () =
@@ -138,7 +137,7 @@ let build_beq_scheme mode kn =
| Name s -> Id.of_string ("eq_"^(Id.to_string s))
| Anonymous -> Id.of_string "eq_A"
in
- let ext_rel_list = extended_rel_list 0 lnamesparrec in
+ let ext_rel_list = Context.Rel.to_extended_list 0 lnamesparrec in
let lift_cnt = ref 0 in
let eqs_typ = List.map (fun aa ->
let a = lift !lift_cnt aa in
@@ -234,7 +233,7 @@ let build_beq_scheme mode kn =
Cn => match Y with ... end |] part *)
let ci = make_case_info env (fst ind) MatchStyle in
let constrs n = get_constructors env (make_ind_family (ind,
- extended_rel_list (n+nb_ind-1) mib.mind_params_ctxt)) in
+ Context.Rel.to_extended_list (n+nb_ind-1) mib.mind_params_ctxt)) in
let constrsi = constrs (3+nparrec) in
let n = Array.length constrsi in
let ar = Array.make n (Lazy.force ff) in
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 22baa5e61..28a39b570 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -12,7 +12,6 @@ open Pp
open Names
open Term
open Vars
-open Context
open Termops
open Entries
open Environ
@@ -198,13 +197,13 @@ let build_id_coercion idf_opt source poly =
let val_f =
it_mkLambda_or_LetIn
(mkLambda (Name Namegen.default_dependent_ident,
- applistc vs (extended_rel_list 0 lams),
+ applistc vs (Context.Rel.to_extended_list 0 lams),
mkRel 1))
lams
in
let typ_f =
it_mkProd_wo_LetIn
- (mkProd (Anonymous, applistc vs (extended_rel_list 0 lams), lift 1 t))
+ (mkProd (Anonymous, applistc vs (Context.Rel.to_extended_list 0 lams), lift 1 t))
lams
in
(* juste pour verification *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 9cdb46064..ab18350c5 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -351,7 +351,7 @@ let context poly l =
let evars = ref (Evd.from_env env) in
let _, ((env', fullctx), impls) = interp_context_evars env evars l in
let subst = Evarutil.evd_comb0 Evarutil.nf_evars_and_universes evars in
- let fullctx = Context.map_rel_context subst fullctx in
+ let fullctx = Context.Rel.map subst fullctx in
let ce t = Evarutil.check_evars env Evd.empty !evars t in
let () = List.iter (fun (n, b, t) -> Option.iter ce b; ce t) fullctx in
let ctx =
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 2b7e9e4fe..80ed24629 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -7,7 +7,6 @@
(************************************************************************)
open Names
-open Context
open Environ
open Constrexpr
open Typeclasses
@@ -15,9 +14,9 @@ open Libnames
(** Errors *)
-val mismatched_params : env -> constr_expr list -> rel_context -> 'a
+val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a
-val mismatched_props : env -> constr_expr list -> rel_context -> 'a
+val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a
(** Instance declaration *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 91cfddb54..500769aca 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -12,7 +12,6 @@ open Util
open Flags
open Term
open Vars
-open Context
open Termops
open Entries
open Environ
@@ -87,7 +86,7 @@ let interp_definition pl bl p red_option c ctypopt =
match ctypopt with
None ->
let subst = evd_comb0 Evd.nf_univ_variables evdref in
- let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_constr_evars_impls ~impls env_bl evdref c in
let nf,subst = Evarutil.e_nf_evars_and_universes evdref in
@@ -100,7 +99,7 @@ let interp_definition pl bl p red_option c ctypopt =
| Some ctyp ->
let ty, impsty = interp_type_evars_impls ~impls env_bl evdref ctyp in
let subst = evd_comb0 Evd.nf_univ_variables evdref in
- let ctx = map_rel_context (Vars.subst_univs_constr subst) ctx in
+ let ctx = Context.Rel.map (Vars.subst_univs_constr subst) ctx in
let env_bl = push_rel_context ctx env in
let c, imps2 = interp_casted_constr_evars_impls ~impls env_bl evdref c ty in
let nf, subst = Evarutil.e_nf_evars_and_universes evdref in
@@ -125,7 +124,7 @@ let interp_definition pl bl p red_option c ctypopt =
definition_entry ~types:typ ~poly:p
~univs:uctx body
in
- red_constant_entry (rel_context_length ctx) ce !evdref red_option, !evdref, pl, imps
+ red_constant_entry (Context.Rel.length ctx) ce !evdref red_option, !evdref, pl, imps
let check_definition (ce, evd, _, imps) =
check_evars_are_solved (Global.env ()) evd (Evd.empty,evd);
@@ -566,7 +565,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
(* Compute interpretation metadatas *)
let indimpls = List.map (fun (_, _, impls) -> userimpls @
- lift_implicits (rel_context_nhyps ctx_params) impls) arities in
+ lift_implicits (Context.Rel.nhyps ctx_params) impls) arities in
let arities = List.map pi1 arities and aritypoly = List.map pi2 arities in
let impls = compute_internalization_env env0 (Inductive params) indnames fullarities indimpls in
let mldatas = List.map2 (mk_mltype_data evdref env_params params) arities indnames in
@@ -592,11 +591,11 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
let nf x = nf' (nf x) in
let arities = List.map nf' arities in
let constructors = List.map (fun (idl,cl,impsl) -> (idl,List.map nf' cl,impsl)) constructors in
- let ctx_params = map_rel_context nf ctx_params in
+ let ctx_params = Context.Rel.map nf ctx_params in
let evd = !evdref in
let pl, uctx = Evd.universe_context ?names:pl evd in
List.iter (check_evars env_params Evd.empty evd) arities;
- iter_rel_context (check_evars env0 Evd.empty evd) ctx_params;
+ Context.Rel.iter (check_evars env0 Evd.empty evd) ctx_params;
List.iter (fun (_,ctyps,_) ->
List.iter (check_evars env_ar_params Evd.empty evd) ctyps)
constructors;
@@ -610,7 +609,7 @@ let interp_mutual_inductive (paramsl,indl) notations poly prv finite =
mind_entry_lc = ctypes
}) indl arities aritypoly constructors in
let impls =
- let len = rel_context_nhyps ctx_params in
+ let len = Context.Rel.nhyps ctx_params in
List.map2 (fun indimpls (_,_,cimpls) ->
indimpls, List.map (fun impls ->
userimpls @ (lift_implicits len impls)) cimpls) indimpls constructors
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index b6da21e5a..9416b7e7a 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -9,7 +9,6 @@
open Names
open Errors
open Util
-open Context
open Term
open Vars
open Entries
@@ -37,8 +36,8 @@ let detype_param = function
let abstract_inductive hyps nparams inds =
let ntyp = List.length inds in
- let nhyp = named_context_length hyps in
- let args = instance_from_named_context (List.rev hyps) in
+ let nhyp = Context.Named.length hyps in
+ let args = Context.Named.to_instance (List.rev hyps) in
let args = Array.of_list args in
let subs = List.init ntyp (fun k -> lift nhyp (mkApp(mkRel (k+1),args))) in
let inds' =
@@ -100,7 +99,7 @@ let process_inductive (sechyps,abs_ctx) modlist mib =
Array.to_list mip.mind_consnames,
Array.to_list lc))
mib.mind_packets in
- let sechyps' = map_named_context (expmod_constr modlist) sechyps in
+ let sechyps' = Context.Named.map (expmod_constr modlist) sechyps in
let (params',inds') = abstract_inductive sechyps' nparams inds in
let abs_ctx = Univ.instantiate_univ_context abs_ctx in
let univs = Univ.UContext.union abs_ctx univs in
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 386e4e3ef..2984a0be8 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -6,10 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Context
open Declarations
open Entries
open Opaqueproof
val process_inductive :
- named_context Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
+ Context.Named.t Univ.in_universe_context -> work_list -> mutual_inductive_body -> mutual_inductive_entry
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index a3b973e4d..fd91cfb5c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -13,7 +13,6 @@ open Declare
*)
open Term
-open Context
open Vars
open Names
open Evd
@@ -44,7 +43,7 @@ let check_evars env evm =
type oblinfo =
{ ev_name: int * Id.t;
- ev_hyps: named_context;
+ ev_hyps: Context.Named.t;
ev_status: Evar_kinds.obligation_definition_status;
ev_chop: int option;
ev_src: Evar_kinds.t Loc.located;
@@ -191,7 +190,7 @@ open Environ
let eterm_obligations env name evm fs ?status t ty =
(* 'Serialize' the evars *)
let nc = Environ.named_context env in
- let nc_len = Context.named_context_length nc in
+ let nc_len = Context.Named.length nc in
let evm = Evarutil.nf_evar_map_undefined evm in
let evl = Evarutil.non_instantiated evm in
let evl = Evar.Map.bindings evl in
diff --git a/toplevel/record.ml b/toplevel/record.ml
index c432274a0..408d3fa5f 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -13,7 +13,6 @@ open Names
open Globnames
open Nameops
open Term
-open Context
open Vars
open Environ
open Declarations
@@ -148,8 +147,8 @@ let typecheck_params_and_fields def id pl t ps nots fs =
else arity, evars
in
let evars, nf = Evarutil.nf_evars_and_universes evars in
- let newps = map_rel_context nf newps in
- let newfs = map_rel_context nf newfs in
+ let newps = Context.Rel.map nf newps in
+ let newfs = Context.Rel.map nf newfs in
let ce t = Evarutil.check_evars env0 Evd.empty evars t in
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newps);
List.iter (fun (n, b, t) -> Option.iter ce b; ce t) (List.rev newfs);
@@ -244,8 +243,8 @@ let declare_projections indsp ?(kind=StructureComponent) binder_name coers field
let ctx = Univ.instantiate_univ_context mib.mind_universes in
let indu = indsp, u in
let r = mkIndU (indsp,u) in
- let rp = applist (r, Context.extended_rel_list 0 paramdecls) in
- let paramargs = Context.extended_rel_list 1 paramdecls in (*def in [[params;x:rp]]*)
+ let rp = applist (r, Context.Rel.to_extended_list 0 paramdecls) in
+ let paramargs = Context.Rel.to_extended_list 1 paramdecls in (*def in [[params;x:rp]]*)
let x = Name binder_name in
let fields = instantiate_possibly_recursive_type indu paramdecls fields in
let lifted_fields = Termops.lift_rel_context 1 fields in
@@ -353,7 +352,7 @@ open Typeclasses
let declare_structure finite poly ctx id idbuild paramimpls params arity template
fieldimpls fields ?(kind=StructureComponent) ?name is_coe coers sign =
let nparams = List.length params and nfields = List.length fields in
- let args = Context.extended_rel_list nfields params in
+ let args = Context.Rel.to_extended_list nfields params in
let ind = applist (mkRel (1+nparams+nfields), args) in
let type_constructor = it_mkProd_or_LetIn ind fields in
let binder_name =
diff --git a/toplevel/record.mli b/toplevel/record.mli
index eccb5d29d..f68adcec8 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -8,7 +8,6 @@
open Names
open Term
-open Context
open Vernacexpr
open Constrexpr
open Impargs
@@ -22,15 +21,15 @@ val primitive_flag : bool ref
val declare_projections :
inductive -> ?kind:Decl_kinds.definition_object_kind -> Id.t ->
- coercion_flag list -> manual_explicitation list list -> rel_context ->
+ coercion_flag list -> manual_explicitation list list -> Context.Rel.t ->
(Name.t * bool) list * constant option list
val declare_structure : Decl_kinds.recursivity_kind ->
bool (** polymorphic?*) -> Univ.universe_context ->
Id.t -> Id.t ->
- manual_explicitation list -> rel_context -> (** params *) constr -> (** arity *)
+ manual_explicitation list -> Context.Rel.t -> (** params *) constr -> (** arity *)
bool (** template arity ? *) ->
- Impargs.manual_explicitation list list -> rel_context -> (** fields *)
+ Impargs.manual_explicitation list list -> Context.Rel.t -> (** fields *)
?kind:Decl_kinds.definition_object_kind -> ?name:Id.t ->
bool -> (** coercion? *)
bool list -> (** field coercions *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7144db494..55e57ec69 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1580,7 +1580,7 @@ let print_about_hyp_globs ref_or_by_not glnumopt =
(str "No such goal: " ++ int n ++ str "."))
| _ , _ -> raise NoHyp in
let hyps = pf_hyps gl in
- let (id,bdyopt,typ) = Context.lookup_named id hyps in
+ let (id,bdyopt,typ) = Context.Named.lookup id hyps in
let natureofid = match bdyopt with
| None -> "Hypothesis"
| Some bdy ->"Constant (let in)" in
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 08:10:29 +0000