diff options
48 files changed, 169 insertions, 153 deletions
diff --git a/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh b/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh new file mode 100644 index 000000000..b4d3d7e67 --- /dev/null +++ b/dev/ci/user-overlays/7080-herbelin-master+swapping-modules-constr-context.sh @@ -0,0 +1,7 @@ +if [ "$CI_PULL_REQUEST" = "7080" ] || [ "$CI_BRANCH" = "master+swapping-modules-constr-context" ]; then + Equations_CI_BRANCH=master+adapting-coq-pr7080 + Equations_CI_GITURL=https://github.com/herbelin/Coq-Equations.git + + Elpi_CI_BRANCH=coq-master+adapting-coq-pr7080 + Elpi_CI_GITURL=https://github.com/herbelin/coq-elpi.git +fi diff --git a/dev/doc/changes.md b/dev/doc/changes.md index f3fc126f9..cbb95625f 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -53,6 +53,16 @@ Printer.ml API pr_subgoal and pr_goal was removed to simplify the code. It was earlierly used by PCoq. +Kernel + + The following renamings happened: + - `Context.Rel.t` into `Constr.rel_context` + - `Context.Named.t` into `Constr.named_context` + - `Context.Compacted.t` into `Constr.compacted_context` + - `Context.Rel.Declaration.t` into `Constr.rel_declaration` + - `Context.Named.Declaration.t` into `Constr.named_declaration` + - `Context.Compacted.Declaration.t` into `Constr.compacted_declaration` + Source code organization - We have eliminated / fused some redundant modules and relocated a diff --git a/engine/eConstr.mli b/engine/eConstr.mli index 913825a9f..ecb36615f 100644 --- a/engine/eConstr.mli +++ b/engine/eConstr.mli @@ -321,7 +321,7 @@ sig val to_named_decl : (t, types) Context.Named.Declaration.pt -> (Constr.t, Constr.types) Context.Named.Declaration.pt (** Physical identity. Does not care for defined evars. *) - val to_named_context : (t, types) Context.Named.pt -> Context.Named.t + val to_named_context : (t, types) Context.Named.pt -> Constr.named_context val to_sorts : ESorts.t -> Sorts.t (** Physical identity. Does not care for normalization. *) diff --git a/engine/evarutil.mli b/engine/evarutil.mli index 8ce1b625f..135aa73fc 100644 --- a/engine/evarutil.mli +++ b/engine/evarutil.mli @@ -128,7 +128,7 @@ val advance : evar_map -> Evar.t -> Evar.t option [nf_evar]. *) val undefined_evars_of_term : evar_map -> constr -> Evar.Set.t -val undefined_evars_of_named_context : evar_map -> Context.Named.t -> Evar.Set.t +val undefined_evars_of_named_context : evar_map -> Constr.named_context -> Evar.Set.t val undefined_evars_of_evar_info : evar_map -> evar_info -> Evar.Set.t type undefined_evars_cache @@ -161,7 +161,7 @@ val jv_nf_evar : val tj_nf_evar : evar_map -> unsafe_type_judgment -> unsafe_type_judgment -val nf_named_context_evar : evar_map -> Context.Named.t -> Context.Named.t +val nf_named_context_evar : evar_map -> Constr.named_context -> Constr.named_context val nf_rel_context_evar : evar_map -> rel_context -> rel_context val nf_env_evar : evar_map -> env -> env diff --git a/engine/evd.mli b/engine/evd.mli index 64db70451..d638bb2d3 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -230,7 +230,7 @@ val existential_opt_value : evar_map -> econstr pexistential -> econstr option val existential_opt_value0 : evar_map -> existential -> constr option -val evar_instance_array : (Context.Named.Declaration.t -> 'a -> bool) -> evar_info -> +val evar_instance_array : (Constr.named_declaration -> 'a -> bool) -> evar_info -> 'a array -> (Id.t * 'a) list val instantiate_evar_array : evar_info -> econstr -> econstr array -> econstr diff --git a/engine/termops.mli b/engine/termops.mli index f9aa6ba63..80988989f 100644 --- a/engine/termops.mli +++ b/engine/termops.mli @@ -43,14 +43,14 @@ val it_mkProd : types -> (Name.t * types) list -> types val it_mkLambda : constr -> (Name.t * types) list -> constr val it_mkProd_or_LetIn : types -> rel_context -> types val it_mkProd_wo_LetIn : types -> rel_context -> types -val it_mkLambda_or_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr val it_mkNamedProd_or_LetIn : types -> named_context -> types -val it_mkNamedProd_wo_LetIn : Constr.types -> Context.Named.t -> Constr.types +val it_mkNamedProd_wo_LetIn : Constr.types -> Constr.named_context -> Constr.types val it_mkNamedLambda_or_LetIn : constr -> named_context -> constr (* Ad hoc version reinserting letin, assuming the body is defined in the context where the letins are expanded *) -val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Context.Rel.t -> Constr.constr +val it_mkLambda_or_LetIn_from_no_LetIn : Constr.constr -> Constr.rel_context -> Constr.constr (** {6 Generic iterators on constr} *) @@ -225,7 +225,7 @@ val names_of_rel_context : env -> names_context (* [context_chop n Γ] returns (Γ₁,Γ₂) such that [Γ]=[Γ₂Γ₁], [Γ₁] has [n] hypotheses, excluding local definitions, and [Γ₁], if not empty, starts with an hypothesis (i.e. [Γ₁] has the form empty or [x:A;Γ₁'] *) -val context_chop : int -> Context.Rel.t -> Context.Rel.t * Context.Rel.t +val context_chop : int -> Constr.rel_context -> Constr.rel_context * Constr.rel_context (* [env_rel_context_chop n env] extracts out the [n] top declarations of the rel_context part of [env], counting both local definitions and @@ -239,19 +239,19 @@ val add_vname : Id.Set.t -> Name.t -> Id.Set.t (** other signature iterators *) val process_rel_context : (rel_declaration -> env -> env) -> env -> env val assums_of_rel_context : ('c, 't) Context.Rel.pt -> (Name.t * 't) list -val lift_rel_context : int -> Context.Rel.t -> Context.Rel.t -val substl_rel_context : Constr.constr list -> Context.Rel.t -> Context.Rel.t -val smash_rel_context : Context.Rel.t -> Context.Rel.t (** expand lets in context *) +val lift_rel_context : int -> Constr.rel_context -> Constr.rel_context +val substl_rel_context : Constr.constr list -> Constr.rel_context -> Constr.rel_context +val smash_rel_context : Constr.rel_context -> Constr.rel_context (** expand lets in context *) val map_rel_context_in_env : - (env -> Constr.constr -> Constr.constr) -> env -> Context.Rel.t -> Context.Rel.t + (env -> Constr.constr -> Constr.constr) -> env -> Constr.rel_context -> Constr.rel_context val map_rel_context_with_binders : (int -> 'c -> 'c) -> ('c, 'c) Context.Rel.pt -> ('c, 'c) Context.Rel.pt val fold_named_context_both_sides : - ('a -> Context.Named.Declaration.t -> Context.Named.Declaration.t list -> 'a) -> - Context.Named.t -> init:'a -> 'a + ('a -> Constr.named_declaration -> Constr.named_declaration list -> 'a) -> + Constr.named_context -> init:'a -> 'a val mem_named_context_val : Id.t -> named_context_val -> bool -val compact_named_context : Context.Named.t -> Context.Compacted.t +val compact_named_context : Constr.named_context -> Constr.compacted_context val map_rel_decl : ('a -> 'b) -> ('a, 'a) Context.Rel.Declaration.pt -> ('b, 'b) Context.Rel.Declaration.pt val map_named_decl : ('a -> 'b) -> ('a, 'a) Context.Named.Declaration.pt -> ('b, 'b) Context.Named.Declaration.pt @@ -313,6 +313,6 @@ val set_print_constr : (env -> Evd.evar_map -> constr -> Pp.t) -> unit val print_constr : constr -> Pp.t val print_constr_env : env -> Evd.evar_map -> constr -> Pp.t val print_named_context : env -> Pp.t -val pr_rel_decl : env -> Context.Rel.Declaration.t -> Pp.t +val pr_rel_decl : env -> Constr.rel_declaration -> Pp.t val print_rel_context : env -> Pp.t val print_env : env -> Pp.t diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 83ad9af33..288a0bfe0 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -22,7 +22,7 @@ open Libobject open Nameops open Context.Rel.Declaration -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) let mismatched_ctx_inst_err env c n m = raise (MismatchedContextInstance (env, c, n, m)) module RelDecl = Context.Rel.Declaration diff --git a/interp/implicit_quantifiers.mli b/interp/implicit_quantifiers.mli index a8492095e..437fef175 100644 --- a/interp/implicit_quantifiers.mli +++ b/interp/implicit_quantifiers.mli @@ -38,14 +38,14 @@ val make_fresh : Id.Set.t -> Environ.env -> Id.t -> Id.t val implicits_of_glob_constr : ?with_products:bool -> Glob_term.glob_constr -> Impargs.manual_implicits val combine_params_freevar : - Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t val implicit_application : Id.Set.t -> ?allow_partial:bool -> - (Id.Set.t -> GlobRef.t option * Context.Rel.Declaration.t -> + (Id.Set.t -> GlobRef.t option * Constr.rel_declaration -> Constrexpr.constr_expr * Id.Set.t) -> constr_expr -> constr_expr * Id.Set.t (* Should be likely located elsewhere *) -exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Context.Rel.t (* found, expected *) -val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Context.Rel.t -> 'a +exception MismatchedContextInstance of Environ.env * Typeclasses_errors.contexts * constr_expr list * Constr.rel_context (* found, expected *) +val mismatched_ctx_inst_err : Environ.env -> Typeclasses_errors.contexts -> constr_expr list -> Constr.rel_context -> 'a diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 1d5142a5c..61ed40394 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -265,7 +265,7 @@ type 'a infos_cache = { i_repr : 'a infos -> 'a infos_tab -> constr -> 'a; i_env : env; i_sigma : existential -> constr option; - i_rels : (Context.Rel.Declaration.t * lazy_val) Range.t; + i_rels : (Constr.rel_declaration * lazy_val) Range.t; } and 'a infos = { diff --git a/kernel/constr.ml b/kernel/constr.ml index 45812b5a1..9bf743152 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1209,3 +1209,10 @@ let hcons = Id.hcons) (* let hcons_types = hcons_constr *) + +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_declaration = (constr, types) Context.Named.Declaration.pt +type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt +type rel_context = rel_declaration list +type named_context = named_declaration list +type compacted_context = compacted_declaration list diff --git a/kernel/constr.mli b/kernel/constr.mli index bf7b5e87b..70acf1932 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -372,6 +372,15 @@ val eq_constr_nounivs : constr -> constr -> bool (** Total ordering compatible with [equal] *) val compare : constr -> constr -> int +(** {6 Extension of Context with declarations on constr} *) + +type rel_declaration = (constr, types) Context.Rel.Declaration.pt +type named_declaration = (constr, types) Context.Named.Declaration.pt +type compacted_declaration = (constr, types) Context.Compacted.Declaration.pt +type rel_context = rel_declaration list +type named_context = named_declaration list +type compacted_context = compacted_declaration list + (** {6 Functionals working on the immediate subterm of a construction } *) (** [fold f acc c] folds [f] on the immediate subterms of [c] diff --git a/kernel/context.ml b/kernel/context.ml index 5d4a10184..831dc850f 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -43,8 +43,6 @@ struct | LocalAssum of Name.t * 'types (** name, type *) | LocalDef of Name.t * 'constr * 'types (** name, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the name bound by a given declaration. *) let get_name = function | LocalAssum (na,_) @@ -157,7 +155,6 @@ struct Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty rel-context *) let empty = [] @@ -241,8 +238,6 @@ struct | LocalAssum of Id.t * 'types (** identifier, type *) | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the identifier bound by a given declaration. *) let get_id = function | LocalAssum (id,_) -> id @@ -370,7 +365,6 @@ struct Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty named-context *) let empty = [] @@ -429,8 +423,6 @@ module Compacted = | LocalAssum of Id.t list * 'types | LocalDef of Id.t list * 'constr * 'types - type t = (Constr.constr, Constr.types) pt - let map_constr f = function | LocalAssum (ids, ty) as decl -> let ty' = f ty in @@ -454,7 +446,6 @@ module Compacted = end type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list let fold f l ~init = List.fold_right f l init end diff --git a/kernel/context.mli b/kernel/context.mli index c97db4348..957ac4b3d 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -35,8 +35,6 @@ sig | LocalAssum of Name.t * 'types (** name, type *) | LocalDef of Name.t * 'constr * 'types (** name, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the name bound by a given declaration. *) val get_name : ('c, 't) pt -> Name.t @@ -93,7 +91,6 @@ sig Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty rel-context *) val empty : ('c, 't) pt @@ -153,8 +150,6 @@ sig | LocalAssum of Id.t * 'types (** identifier, type *) | LocalDef of Id.t * 'constr * 'types (** identifier, value, type *) - type t = (Constr.constr, Constr.types) pt - (** Return the identifier bound by a given declaration. *) val get_id : ('c, 't) pt -> Id.t @@ -220,7 +215,6 @@ sig Inner-most declarations are at the beginning of the list. Outer-most declarations are at the end of the list. *) type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list (** empty named-context *) val empty : ('c, 't) pt @@ -270,15 +264,12 @@ sig | LocalAssum of Id.t list * 'types | LocalDef of Id.t list * 'constr * 'types - type t = (Constr.constr, Constr.types) pt - val map_constr : ('c -> 'c) -> ('c, 'c) pt -> ('c, 'c) pt val of_named_decl : ('c, 't) Named.Declaration.pt -> ('c, 't) pt val to_named_context : ('c, 't) pt -> ('c, 't) Named.pt end type ('constr, 'types) pt = ('constr, 'types) Declaration.pt list - type t = Declaration.t list val fold : (('c, 't) Declaration.pt -> 'a -> 'a) -> ('c, 't) pt -> init:'a -> 'a end diff --git a/kernel/cooking.ml b/kernel/cooking.ml index c7a84f617..521a7d890 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -157,7 +157,7 @@ type result = { cook_type : types; cook_universes : constant_universes; cook_inline : inline; - cook_context : Context.Named.t option; + cook_context : Constr.named_context option; } let on_body ml hy f = function diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 76c79335f..4c254d2ea 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -23,7 +23,7 @@ type result = { cook_type : types; cook_universes : constant_universes; cook_inline : inline; - cook_context : Context.Named.t option; + cook_context : Constr.named_context option; } val cook_constant : hcons:bool -> env -> recipe -> result diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 58fb5d66b..95078800e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -80,7 +80,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaqueDef *) type constant_body = { - const_hyps : Context.Named.t; (** New: younger hyp at top *) + const_hyps : Constr.named_context; (** New: younger hyp at top *) const_body : constant_def; const_type : types; const_body_code : Cemitcodes.to_patch_substituted option; @@ -138,7 +138,7 @@ type one_inductive_body = { mind_typename : Id.t; (** Name of the type: [Ii] *) - mind_arity_ctxt : Context.Rel.t; (** Arity context of [Ii] with parameters: [forall params, Ui] *) + mind_arity_ctxt : Constr.rel_context; (** Arity context of [Ii] with parameters: [forall params, Ui] *) mind_arity : inductive_arity; (** Arity sort and original user arity *) @@ -196,13 +196,13 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.Named.t; (** Section hypotheses on which the block depends *) + mind_hyps : Constr.named_context; (** Section hypotheses on which the block depends *) mind_nparams : int; (** Number of expected parameters including non-uniform ones (i.e. length of mind_params_ctxt w/o let-in) *) mind_nparams_rec : int; (** Number of recursively uniform (i.e. ordinary) parameters *) - mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *) + mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *) mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) diff --git a/kernel/entries.ml b/kernel/entries.ml index 724ed9ec7..40873bea7 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -75,7 +75,7 @@ type 'a in_constant_universes_entry = 'a * constant_universes_entry type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.Named.t option; + const_entry_secctx : Constr.named_context option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -85,7 +85,7 @@ type 'a definition_entry = { type section_def_entry = { secdef_body : constr; - secdef_secctx : Context.Named.t option; + secdef_secctx : Constr.named_context option; secdef_feedback : Stateid.t option; secdef_type : types option; } @@ -93,7 +93,7 @@ type section_def_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.Named.t option * types in_constant_universes_entry * inline + Constr.named_context option * types in_constant_universes_entry * inline type 'a constant_entry = | DefinitionEntry of 'a definition_entry diff --git a/kernel/environ.ml b/kernel/environ.ml index 224b6d5b8..4ab469803 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -77,13 +77,13 @@ let dummy_lazy_val () = ref VKnone let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key) type named_context_val = { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; + env_named_ctx : Constr.named_context; + env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; } type rel_context_val = { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; + env_rel_ctx : Constr.rel_context; + env_rel_map : (Constr.rel_declaration * lazy_val) Range.t; } type env = { diff --git a/kernel/environ.mli b/kernel/environ.mli index 084d3c4de..0259dbbdd 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -55,13 +55,13 @@ type stratification = { } type named_context_val = private { - env_named_ctx : Context.Named.t; - env_named_map : (Context.Named.Declaration.t * lazy_val) Id.Map.t; + env_named_ctx : Constr.named_context; + env_named_map : (Constr.named_declaration * lazy_val) Id.Map.t; } type rel_context_val = private { - env_rel_ctx : Context.Rel.t; - env_rel_map : (Context.Rel.Declaration.t * lazy_val) Range.t; + env_rel_ctx : Constr.rel_context; + env_rel_map : (Constr.rel_declaration * lazy_val) Range.t; } type env = private { @@ -83,8 +83,8 @@ val eq_named_context_val : named_context_val -> named_context_val -> bool val empty_env : env val universes : env -> UGraph.t -val rel_context : env -> Context.Rel.t -val named_context : env -> Context.Named.t +val rel_context : env -> Constr.rel_context +val named_context : env -> Constr.named_context val named_context_val : env -> named_context_val val opaque_tables : env -> Opaqueproof.opaquetab @@ -103,13 +103,13 @@ val empty_context : env -> bool (** {5 Context of de Bruijn variables ([rel_context]) } *) val nb_rel : env -> int -val push_rel : Context.Rel.Declaration.t -> env -> env -val push_rel_context : Context.Rel.t -> env -> env +val push_rel : Constr.rel_declaration -> env -> env +val push_rel_context : Constr.rel_context -> env -> env val push_rec_types : rec_declaration -> env -> env (** Looks up in the context of local vars referred by indice ([rel_context]) raises [Not_found] if the index points out of the context *) -val lookup_rel : int -> env -> Context.Rel.Declaration.t +val lookup_rel : int -> env -> Constr.rel_declaration val lookup_rel_val : int -> env -> lazy_val val evaluable_rel : int -> env -> bool val env_of_rel : int -> env -> env @@ -117,12 +117,12 @@ val env_of_rel : int -> env -> env (** {6 Recurrence on [rel_context] } *) val fold_rel_context : - (env -> Context.Rel.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Constr.rel_declaration -> 'a -> 'a) -> env -> init:'a -> 'a (** {5 Context of variables (section variables and goal assumptions) } *) -val named_context_of_val : named_context_val -> Context.Named.t -val val_of_named_context : Context.Named.t -> named_context_val +val named_context_of_val : named_context_val -> Constr.named_context +val val_of_named_context : Constr.named_context -> named_context_val val empty_named_context_val : named_context_val val ids_of_named_context_val : named_context_val -> Id.Set.t @@ -133,19 +133,19 @@ val ids_of_named_context_val : named_context_val -> Id.Set.t val map_named_val : (constr -> constr) -> named_context_val -> named_context_val -val push_named : Context.Named.Declaration.t -> env -> env -val push_named_context : Context.Named.t -> env -> env +val push_named : Constr.named_declaration -> env -> env +val push_named_context : Constr.named_context -> env -> env val push_named_context_val : - Context.Named.Declaration.t -> named_context_val -> named_context_val + Constr.named_declaration -> named_context_val -> named_context_val (** Looks up in the context of local vars referred by names ([named_context]) raises [Not_found] if the Id.t is not found *) -val lookup_named : variable -> env -> Context.Named.Declaration.t +val lookup_named : variable -> env -> Constr.named_declaration val lookup_named_val : variable -> env -> lazy_val -val lookup_named_ctxt : variable -> named_context_val -> Context.Named.Declaration.t +val lookup_named_ctxt : variable -> named_context_val -> Constr.named_declaration val evaluable_named : variable -> env -> bool val named_type : variable -> env -> types val named_body : variable -> env -> constr option @@ -153,13 +153,13 @@ val named_body : variable -> env -> constr option (** {6 Recurrence on [named_context]: older declarations processed first } *) val fold_named_context : - (env -> Context.Named.Declaration.t -> 'a -> 'a) -> env -> init:'a -> 'a + (env -> Constr.named_declaration -> 'a -> 'a) -> env -> init:'a -> 'a val set_universes : env -> UGraph.t -> env (** Recurrence on [named_context] starting from younger decl *) val fold_named_context_reverse : - ('a -> Context.Named.Declaration.t -> 'a) -> init:'a -> env -> 'a + ('a -> Constr.named_declaration -> 'a) -> init:'a -> env -> 'a (** This forgets named and rel contexts *) val reset_context : env -> env @@ -278,7 +278,7 @@ val vars_of_global : env -> constr -> Id.Set.t val really_needed : env -> Id.Set.t -> Id.Set.t (** like [really_needed] but computes a well ordered named context *) -val keep_hyps : env -> Id.Set.t -> Context.Named.t +val keep_hyps : env -> Id.Set.t -> Constr.named_context (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is @@ -307,10 +307,10 @@ exception Hyp_not_found return [tail::(f head (id,_,_) (rev tail))::head]. the value associated to id should not change *) val apply_to_hyp : named_context_val -> variable -> - (Context.Named.t -> Context.Named.Declaration.t -> Context.Named.t -> Context.Named.Declaration.t) -> + (Constr.named_context -> Constr.named_declaration -> Constr.named_context -> Constr.named_declaration) -> named_context_val -val remove_hyps : Id.Set.t -> (Context.Named.Declaration.t -> Context.Named.Declaration.t) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val +val remove_hyps : Id.Set.t -> (Constr.named_declaration -> Constr.named_declaration) -> (lazy_val -> lazy_val) -> named_context_val -> named_context_val diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index e63f43849..61b71df31 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -425,7 +425,7 @@ let typecheck_inductive env mie = type ill_formed_ind = | LocalNonPos of int | LocalNotEnoughArgs of int - | LocalNotConstructor of Context.Rel.t * int + | LocalNotConstructor of Constr.rel_context * int | LocalNonPar of int * int * int exception IllFormedInd of ill_formed_ind diff --git a/kernel/inductive.mli b/kernel/inductive.mli index c7982f1fc..3c1464c6c 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -36,7 +36,7 @@ val lookup_mind_specif : env -> inductive -> mind_specif (** {6 Functions to build standard types related to inductive } *) val ind_subst : MutInd.t -> mutual_inductive_body -> Instance.t -> constr list -val inductive_paramdecls : mutual_inductive_body puniverses -> Context.Rel.t +val inductive_paramdecls : mutual_inductive_body puniverses -> Constr.rel_context val instantiate_inductive_constraints : mutual_inductive_body -> Instance.t -> Constraint.t @@ -87,7 +87,7 @@ val build_branches_type : constr list -> constr -> types array (** Return the arity of an inductive type *) -val mind_arity : one_inductive_body -> Context.Rel.t * Sorts.family +val mind_arity : one_inductive_body -> Constr.rel_context * Sorts.family val inductive_sort_family : one_inductive_body -> Sorts.family @@ -115,8 +115,8 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : env -> Context.Rel.t -> - template_arity -> constr Lazy.t array -> Context.Rel.t * Sorts.t +val instantiate_universes : env -> Constr.rel_context -> + template_arity -> constr Lazy.t array -> Constr.rel_context * Sorts.t (** {6 Debug} *) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index 50713b957..07a02f6ef 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -5,8 +5,8 @@ UGraph Esubst Sorts Evar -Constr Context +Constr Vars Term Mod_subst diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index a484c08e8..f8b71e456 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -18,7 +18,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t } + abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } type proofterm = (constr * Univ.ContextSet.t) Future.computation type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index b6ae80b46..5ea6da649 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -51,7 +51,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t * type cooking_info = { modlist : work_list; - abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t } + abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } (* The type has two caveats: 1) cook_constr is defined after diff --git a/kernel/reduction.mli b/kernel/reduction.mli index e53ab6aef..581e8bd88 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -116,10 +116,10 @@ val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> Context.Rel.t * types -val dest_prod_assum : env -> types -> Context.Rel.t * types -val dest_lam : env -> types -> Context.Rel.t * constr -val dest_lam_assum : env -> types -> Context.Rel.t * types +val dest_prod : env -> types -> Constr.rel_context * types +val dest_prod_assum : env -> types -> Constr.rel_context * types +val dest_lam : env -> constr -> Constr.rel_context * constr +val dest_lam_assum : env -> constr -> Constr.rel_context * constr exception NotArity diff --git a/kernel/term.ml b/kernel/term.ml index 81e344e73..4851a9c0d 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -336,7 +336,7 @@ let strip_lam_n n t = snd (decompose_lam_n n t) Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * Sorts.t +type arity = Constr.rel_context * Sorts.t let destArity = let open Context.Rel.Declaration in diff --git a/kernel/term.mli b/kernel/term.mli index 4d340399d..181d714ed 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -25,14 +25,14 @@ val mkNamedLetIn : Id.t -> constr -> types -> constr -> constr val mkNamedProd : Id.t -> types -> types -> types (** Constructs either [(x:t)c] or [[x=b:t]c] *) -val mkProd_or_LetIn : Context.Rel.Declaration.t -> types -> types -val mkProd_wo_LetIn : Context.Rel.Declaration.t -> types -> types -val mkNamedProd_or_LetIn : Context.Named.Declaration.t -> types -> types -val mkNamedProd_wo_LetIn : Context.Named.Declaration.t -> types -> types +val mkProd_or_LetIn : Constr.rel_declaration -> types -> types +val mkProd_wo_LetIn : Constr.rel_declaration -> types -> types +val mkNamedProd_or_LetIn : Constr.named_declaration -> types -> types +val mkNamedProd_wo_LetIn : Constr.named_declaration -> types -> types (** Constructs either [[x:t]c] or [[x=b:t]c] *) -val mkLambda_or_LetIn : Context.Rel.Declaration.t -> constr -> constr -val mkNamedLambda_or_LetIn : Context.Named.Declaration.t -> constr -> constr +val mkLambda_or_LetIn : Constr.rel_declaration -> constr -> constr +val mkNamedLambda_or_LetIn : Constr.named_declaration -> constr -> constr (** {5 Other term constructors. } *) @@ -74,8 +74,8 @@ val to_lambda : int -> constr -> constr where [l] is [fun (x_1:T_1)...(x_n:T_n) => T] *) val to_prod : int -> constr -> constr -val it_mkLambda_or_LetIn : constr -> Context.Rel.t -> constr -val it_mkProd_or_LetIn : types -> Context.Rel.t -> types +val it_mkLambda_or_LetIn : constr -> Constr.rel_context -> constr +val it_mkProd_or_LetIn : types -> Constr.rel_context -> types (** In [lambda_applist c args], [c] is supposed to have the form [λΓ.c] with [Γ] without let-in; it returns [c] with the variables @@ -126,29 +126,29 @@ val decompose_lam_n : int -> constr -> (Name.t * constr) list * constr (** Extract the premisses and the conclusion of a term of the form "(xi:Ti) ... (xj:=cj:Tj) ..., T" where T is not a product nor a let *) -val decompose_prod_assum : types -> Context.Rel.t * types +val decompose_prod_assum : types -> Constr.rel_context * types (** Idem with lambda's and let's *) -val decompose_lam_assum : constr -> Context.Rel.t * constr +val decompose_lam_assum : constr -> Constr.rel_context * constr (** Idem but extract the first [n] premisses, counting let-ins. *) -val decompose_prod_n_assum : int -> types -> Context.Rel.t * types +val decompose_prod_n_assum : int -> types -> Constr.rel_context * types (** Idem for lambdas, _not_ counting let-ins *) -val decompose_lam_n_assum : int -> constr -> Context.Rel.t * constr +val decompose_lam_n_assum : int -> constr -> Constr.rel_context * constr (** Idem, counting let-ins *) -val decompose_lam_n_decls : int -> constr -> Context.Rel.t * constr +val decompose_lam_n_decls : int -> constr -> Constr.rel_context * constr (** Return the premisses/parameters of a type/term (let-in included) *) -val prod_assum : types -> Context.Rel.t -val lam_assum : constr -> Context.Rel.t +val prod_assum : types -> Constr.rel_context +val lam_assum : constr -> Constr.rel_context (** Return the first n-th premisses/parameters of a type (let included and counted) *) -val prod_n_assum : int -> types -> Context.Rel.t +val prod_n_assum : int -> types -> Constr.rel_context (** Return the first n-th premisses/parameters of a term (let included but not counted) *) -val lam_n_assum : int -> constr -> Context.Rel.t +val lam_n_assum : int -> constr -> Constr.rel_context (** Remove the premisses/parameters of a type/term *) val strip_prod : types -> types @@ -167,7 +167,7 @@ val strip_lam_assum : constr -> constr Such a term can canonically be seen as the pair of a context of types and of a sort *) -type arity = Context.Rel.t * Sorts.t +type arity = Constr.rel_context * Sorts.t (** Build an "arity" from its canonical form *) val mkArity : arity -> types diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 3b2abc777..57acdfe4b 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -28,7 +28,7 @@ val infer_v : env -> constr array -> unsafe_judgment array val infer_type : env -> types -> unsafe_type_judgment val infer_local_decls : - env -> (Id.t * local_entry) list -> (env * Context.Rel.t) + env -> (Id.t * local_entry) list -> (env * Constr.rel_context) (** {6 Basic operations of the typing machine. } *) @@ -102,4 +102,4 @@ val judge_of_case : env -> case_info val type_of_constant_in : env -> pconstant -> types (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Context.Named.t -> unit +val check_hyps_inclusion : env -> ('a -> constr) -> 'a -> Constr.named_context -> unit diff --git a/kernel/vars.mli b/kernel/vars.mli index a0c7ba4bd..fdddbdb34 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -70,10 +70,10 @@ type substl = constr list as if usable in [applist] while the substitution is represented the other way round, i.e. ending with either [u₁] or [c₁], as if usable for [substl]. *) -val subst_of_rel_context_instance : Context.Rel.t -> constr list -> substl +val subst_of_rel_context_instance : Constr.rel_context -> constr list -> substl (** For compatibility: returns the substitution reversed *) -val adjust_subst_to_rel_context : Context.Rel.t -> constr list -> constr list +val adjust_subst_to_rel_context : Constr.rel_context -> constr list -> constr list (** Take an index in an instance of a context and returns its index wrt to the full context (e.g. 2 in [x:A;y:=b;z:C] is 3, i.e. a reference to z) *) @@ -97,13 +97,13 @@ val subst1 : constr -> constr -> constr accordingly indexes in [a₁],...,[an] and [c]. In terms of typing, if Γ ⊢ a{_n}..a₁ : Δ and Γ, Δ, Γ', Ω ⊢ with |Γ'|=[k], then Γ, Γ', [substnl_decl [a₁;...;an]] k Ω ⊢. *) -val substnl_decl : substl -> int -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val substnl_decl : substl -> int -> Constr.rel_declaration -> Constr.rel_declaration (** [substl_decl σ Ω] is a short-hand for [substnl_decl σ 0 Ω] *) -val substl_decl : substl -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val substl_decl : substl -> Constr.rel_declaration -> Constr.rel_declaration (** [subst1_decl a Ω] is a short-hand for [substnl_decl [a] 0 Ω] *) -val subst1_decl : constr -> Context.Rel.Declaration.t -> Context.Rel.Declaration.t +val subst1_decl : constr -> Constr.rel_declaration -> Constr.rel_declaration (** [replace_vars k [(id₁,c₁);...;(idn,cn)] t] substitutes [Var idj] by [cj] in [t]. *) @@ -134,8 +134,8 @@ open Univ (** Level substitutions for polymorphism. *) val subst_univs_level_constr : universe_level_subst -> constr -> constr -val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Context.Rel.t +val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context -> Constr.rel_context (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr -val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t +val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context diff --git a/library/global.mli b/library/global.mli index 57e173cb9..b2a191cee 100644 --- a/library/global.mli +++ b/library/global.mli @@ -23,7 +23,7 @@ val env_is_initial : unit -> bool val universes : unit -> UGraph.t val named_context_val : unit -> Environ.named_context_val -val named_context : unit -> Context.Named.t +val named_context : unit -> Constr.named_context (** {6 Enriching the global environment } *) @@ -79,7 +79,7 @@ val add_module_parameter : (** {6 Queries in the global environment } *) -val lookup_named : variable -> Context.Named.Declaration.t +val lookup_named : variable -> Constr.named_declaration val lookup_constant : Constant.t -> Declarations.constant_body val lookup_inductive : inductive -> Declarations.mutual_inductive_body * Declarations.one_inductive_body diff --git a/library/lib.ml b/library/lib.ml index 128b27e75..a20de55bf 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -405,7 +405,7 @@ let find_opening_node id = - the list of substitution to do at section closing *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = { diff --git a/library/lib.mli b/library/lib.mli index 1d77212e9..5abfccfc7 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -9,6 +9,7 @@ (************************************************************************) open Names + (** Lib: record of operations, backtrack, low-level sections *) (** This module provides a general mechanism to keep a trace of all operations @@ -153,7 +154,7 @@ val unfreeze : frozen -> unit val init : unit -> unit (** {6 Section management for discharge } *) -type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind +type variable_info = Constr.named_declaration * Decl_kinds.binding_kind type variable_context = variable_info list type abstr_info = private { abstr_ctx : variable_context; @@ -165,7 +166,7 @@ type abstr_info = private { } val instance_from_variable_context : variable_context -> Id.t array -val named_of_variable_context : variable_context -> Context.Named.t +val named_of_variable_context : variable_context -> Constr.named_context val section_segment_of_constant : Constant.t -> abstr_info val section_segment_of_mutual_inductive: MutInd.t -> abstr_info @@ -179,9 +180,9 @@ val is_in_section : GlobRef.t -> bool val add_section_variable : Id.t -> Decl_kinds.binding_kind -> Decl_kinds.polymorphic -> Univ.ContextSet.t -> unit val add_section_context : Univ.ContextSet.t -> unit val add_section_constant : Decl_kinds.polymorphic -> - Constant.t -> Context.Named.t -> unit + Constant.t -> Constr.named_context -> unit val add_section_kn : Decl_kinds.polymorphic -> - MutInd.t -> Context.Named.t -> unit + MutInd.t -> Constr.named_context -> unit val replacement_context : unit -> Opaqueproof.work_list (** {6 Discharge: decrease the section level if in the current section } *) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index efb205182..576073344 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -303,7 +303,7 @@ type constructor_summary = { cs_cstr : pconstructor; cs_params : constr list; cs_nargs : int; - cs_args : Context.Rel.t; + cs_args : Constr.rel_context; cs_concl_realargs : constr array } diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index aa53f7e67..8eaef24c4 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -93,12 +93,12 @@ val inductive_nparamdecls : inductive -> int val inductive_nparamdecls_env : env -> inductive -> int (** @return params context *) -val inductive_paramdecls : pinductive -> Context.Rel.t -val inductive_paramdecls_env : env -> pinductive -> Context.Rel.t +val inductive_paramdecls : pinductive -> Constr.rel_context +val inductive_paramdecls_env : env -> pinductive -> Constr.rel_context (** @return full arity context, hence with letin *) -val inductive_alldecls : pinductive -> Context.Rel.t -val inductive_alldecls_env : env -> pinductive -> Context.Rel.t +val inductive_alldecls : pinductive -> Constr.rel_context +val inductive_alldecls_env : env -> pinductive -> Constr.rel_context (** {7 Extract information from a constructor name} *) @@ -141,7 +141,7 @@ type constructor_summary = { cs_cstr : pconstructor; (* internal name of the constructor plus universes *) cs_params : constr list; (* parameters of the constructor in current ctx *) cs_nargs : int; (* length of arguments signature (letin included) *) - cs_args : Context.Rel.t; (* signature of the arguments (letin included) *) + cs_args : Constr.rel_context; (* signature of the arguments (letin included) *) cs_concl_realargs : constr array; (* actual realargs in the concl of cstr *) } val lift_constructor : int -> constructor_summary -> constructor_summary @@ -154,7 +154,7 @@ val get_projections : env -> inductive_family -> Constant.t array option (** [get_arity] returns the arity of the inductive family instantiated with the parameters; if recursively non-uniform parameters are not part of the inductive family, they appears in the arity *) -val get_arity : env -> inductive_family -> Context.Rel.t * Sorts.family +val get_arity : env -> inductive_family -> Constr.rel_context * Sorts.family val build_dependent_constructor : constructor_summary -> constr val build_dependent_inductive : env -> inductive_family -> constr diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index d3aa7ac64..efb3c339a 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -74,10 +74,10 @@ type typeclass = { cl_impl : GlobRef.t; (* Context in which the definitions are typed. Includes both typeclass parameters and superclasses. *) - cl_context : GlobRef.t option list * Context.Rel.t; + cl_context : GlobRef.t option list * Constr.rel_context; (* Context of definitions and properties on defs, will not be shared *) - cl_props : Context.Rel.t; + cl_props : Constr.rel_context; (* The method implementaions as projections. *) cl_projs : (Name.t * (direction * hint_info) option diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index e4a56960c..80c6d8239 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -35,10 +35,10 @@ type typeclass = { (** Context in which the definitions are typed. Includes both typeclass parameters and superclasses. The global reference gives a direct link to the class itself. *) - cl_context : GlobRef.t option list * Context.Rel.t; + cl_context : GlobRef.t option list * Constr.rel_context; (** Context of definitions and properties on defs, will not be shared *) - cl_props : Context.Rel.t; + cl_props : Constr.rel_context; (** The methods implementations of the typeclass as projections. Some may be undefinable due to sorting restrictions or simply undefined if diff --git a/printing/prettyp.ml b/printing/prettyp.ml index f926e8275..fd7135b6a 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -40,7 +40,7 @@ type object_pr = { print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 8dd729610..1668bce29 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -89,7 +89,7 @@ type object_pr = { print_syntactic_def : env -> KerName.t -> Pp.t; print_module : bool -> ModPath.t -> Pp.t; print_modtype : ModPath.t -> Pp.t; - print_named_decl : env -> Evd.evar_map -> Context.Named.Declaration.t -> Pp.t; + print_named_decl : env -> Evd.evar_map -> Constr.named_declaration -> Pp.t; print_library_entry : env -> Evd.evar_map -> bool -> (object_name * Lib.node) -> Pp.t option; print_context : env -> Evd.evar_map -> bool -> int option -> Lib.library_segment -> Pp.t; print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; diff --git a/printing/printer.ml b/printing/printer.ml index d76bd1e2b..92224c992 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -852,7 +852,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t diff --git a/printing/printer.mli b/printing/printer.mli index 7a8b963d2..eddfef6fa 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -152,13 +152,13 @@ val get_compact_context : unit -> bool val pr_context_unlimited : env -> evar_map -> Pp.t val pr_ne_context_of : Pp.t -> env -> evar_map -> Pp.t -val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> Pp.t -val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t -val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t +val pr_named_decl : env -> evar_map -> Constr.named_declaration -> Pp.t +val pr_compacted_decl : env -> evar_map -> Constr.compacted_declaration -> Pp.t +val pr_rel_decl : env -> evar_map -> Constr.rel_declaration -> Pp.t -val pr_named_context : env -> evar_map -> Context.Named.t -> Pp.t +val pr_named_context : env -> evar_map -> Constr.named_context -> Pp.t val pr_named_context_of : env -> evar_map -> Pp.t -val pr_rel_context : env -> evar_map -> Context.Rel.t -> Pp.t +val pr_rel_context : env -> evar_map -> Constr.rel_context -> Pp.t val pr_rel_context_of : env -> evar_map -> Pp.t val pr_context_of : env -> evar_map -> Pp.t @@ -210,7 +210,7 @@ type axiom = type context_object = | Variable of Id.t (* A section variable or a Let definition *) - | Axiom of axiom * (Label.t * Context.Rel.t * types) list + | Axiom of axiom * (Label.t * Constr.rel_context * types) list | Opaque of Constant.t (* An opaque constant. *) | Transparent of Constant.t diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 47c9c51ee..7e250faa8 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -93,7 +93,7 @@ type pstate = { pid : Id.t; (* the name of the theorem whose proof is being constructed *) terminator : proof_terminator CEphemeron.key; endline_tactic : Genarg.glob_generic_argument option; - section_vars : Context.Named.t option; + section_vars : Constr.named_context option; proof : Proof.t; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 9e07ed2d0..854ceaa41 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -126,8 +126,8 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit * (w.r.t. type dependencies and let-ins covered by it) + a list of * ids to be cleared *) val set_used_variables : - Names.Id.t list -> Context.Named.t * Names.lident list -val get_used_variables : unit -> Context.Named.t option + Names.Id.t list -> Constr.named_context * Names.lident list +val get_used_variables : unit -> Constr.named_context option (** Get the universe declaration associated to the current proof. *) val get_universe_decl : unit -> UState.universe_decl diff --git a/vernac/assumptions.mli b/vernac/assumptions.mli index 0e2b0c80e..751e79d89 100644 --- a/vernac/assumptions.mli +++ b/vernac/assumptions.mli @@ -23,7 +23,7 @@ open Printer val traverse : Label.t -> constr -> (Refset_env.t * Refset_env.t Refmap_env.t * - (Label.t * Context.Rel.t * types) list Refmap_env.t) + (Label.t * Constr.rel_context * 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/vernac/classes.mli b/vernac/classes.mli index bd30b2d60..9c37364cb 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -16,9 +16,9 @@ open Libnames (** Errors *) -val mismatched_params : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_params : env -> constr_expr list -> Constr.rel_context -> 'a -val mismatched_props : env -> constr_expr list -> Context.Rel.t -> 'a +val mismatched_props : env -> constr_expr list -> Constr.rel_context -> 'a (** Instance declaration *) diff --git a/vernac/comFixpoint.mli b/vernac/comFixpoint.mli index f51bfbad5..b1a9c8a5a 100644 --- a/vernac/comFixpoint.mli +++ b/vernac/comFixpoint.mli @@ -82,12 +82,12 @@ val interp_fixpoint : val declare_fixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> Proof_global.lemma_possible_guards -> decl_notation list -> unit val declare_cofixpoint : locality -> polymorphic -> recursive_preentry * UState.universe_decl * UState.t * - (Context.Rel.t * Impargs.manual_implicits * int option) list -> + (Constr.rel_context * Impargs.manual_implicits * int option) list -> decl_notation list -> unit (** Very private function, do not use *) diff --git a/vernac/himsg.mli b/vernac/himsg.mli index 1d3807502..91caddcf1 100644 --- a/vernac/himsg.mli +++ b/vernac/himsg.mli @@ -25,7 +25,7 @@ val explain_pretype_error : env -> Evd.evar_map -> pretype_error -> Pp.t val explain_inductive_error : inductive_error -> Pp.t -val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Context.Rel.t -> Pp.t +val explain_mismatched_contexts : env -> contexts -> Constrexpr.constr_expr list -> Constr.rel_context -> Pp.t val explain_typeclass_error : env -> typeclass_error -> Pp.t diff --git a/vernac/obligations.ml b/vernac/obligations.ml index fa6a9adf1..1f401b4e1 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -40,7 +40,7 @@ let check_evars env evm = type oblinfo = { ev_name: int * Id.t; - ev_hyps: Context.Named.t; + ev_hyps: Constr.named_context; ev_status: bool * Evar_kinds.obligation_definition_status; ev_chop: int option; ev_src: Evar_kinds.t Loc.located; diff --git a/vernac/record.mli b/vernac/record.mli index 7cf7da1e2..567f2b313 100644 --- a/vernac/record.mli +++ b/vernac/record.mli @@ -22,7 +22,7 @@ val declare_projections : bool list -> UnivNames.universe_binders -> Impargs.manual_implicits list -> - Context.Rel.t -> + Constr.rel_context -> (Name.t * bool) list * Constant.t option list val definition_structure : |