diff options
| -rw-r--r-- | dev/doc/changes.txt | 4 | ||||
| -rw-r--r-- | kernel/context.ml | 2 | ||||
| -rw-r--r-- | kernel/context.mli | 2 | ||||
| -rw-r--r-- | kernel/cooking.ml | 2 | ||||
| -rw-r--r-- | kernel/cooking.mli | 2 | ||||
| -rw-r--r-- | kernel/declarations.mli | 4 | ||||
| -rw-r--r-- | kernel/entries.mli | 4 | ||||
| -rw-r--r-- | kernel/environ.mli | 2 | ||||
| -rw-r--r-- | kernel/typeops.mli | 2 | ||||
| -rw-r--r-- | proofs/pfedit.mli | 4 | ||||
| -rw-r--r-- | proofs/proof_global.ml | 2 | ||||
| -rw-r--r-- | proofs/proof_global.mli | 4 |
12 files changed, 17 insertions, 17 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index 7b0ba1700..5933649da 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -7,6 +7,10 @@ We renamed the following functions: Context.Rel.Declaration.fold -> Context.Rel.Declaration.fold_constr Context.Named.Declaration.fold -> Context.Named.Declaration.fold_constr +The following type aliases where removed + + Context.section_context ... it was just an alias for "Context.Named.t" which is still available + ========================================= = CHANGES BETWEEN COQ V8.5 AND COQ V8.6 = ========================================= diff --git a/kernel/context.ml b/kernel/context.ml index 4c88283ca..94fcfb486 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -428,5 +428,3 @@ module NamedList = let fold f l ~init = List.fold_right f l init end - -type section_context = Named.t diff --git a/kernel/context.mli b/kernel/context.mli index 8ed09794b..c5da51381 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -263,5 +263,3 @@ sig val fold : (Declaration.t -> 'a -> 'a) -> t -> init:'a -> 'a end - -type section_context = Named.t diff --git a/kernel/cooking.ml b/kernel/cooking.ml index db09e5ed7..f5059cd75 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -154,7 +154,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option let on_body ml hy f = function | Undef _ as x -> x diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 327e697d2..eb4073096 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -19,7 +19,7 @@ type inline = bool type result = constant_def * constant_type * projection_body option * bool * constant_universes * inline - * Context.section_context option + * Context.Named.t option val cook_constant : env -> recipe -> result val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr diff --git a/kernel/declarations.mli b/kernel/declarations.mli index f89773fcc..fe2fa6d7f 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -78,7 +78,7 @@ type typing_flags = { (* some contraints are in constant_constraints, some other may be in * the OpaueDef *) type constant_body = { - const_hyps : Context.section_context; (** New: younger hyp at top *) + const_hyps : Context.Named.t; (** New: younger hyp at top *) const_body : constant_def; const_type : constant_type; const_body_code : Cemitcodes.to_patch_substituted option; @@ -177,7 +177,7 @@ type mutual_inductive_body = { mind_ntypes : int; (** Number of types in the block *) - mind_hyps : Context.section_context; (** Section hypotheses on which the block depends *) + mind_hyps : Context.Named.t; (** 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) *) diff --git a/kernel/entries.mli b/kernel/entries.mli index df2c4653f..b736b2113 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -61,7 +61,7 @@ type 'a const_entry_body = 'a proof_output Future.computation type 'a definition_entry = { const_entry_body : 'a const_entry_body; (* List of section variables *) - const_entry_secctx : Context.section_context option; + const_entry_secctx : Context.Named.t option; (* State id on which the completion of type checking is reported *) const_entry_feedback : Stateid.t option; const_entry_type : types option; @@ -73,7 +73,7 @@ type 'a definition_entry = { type inline = int option (* inlining level, None for no inlining *) type parameter_entry = - Context.section_context option * bool * types Univ.in_universe_context * inline + Context.Named.t option * bool * types Univ.in_universe_context * inline type projection_entry = { proj_entry_ind : mutual_inductive; diff --git a/kernel/environ.mli b/kernel/environ.mli index b5e576435..77451d8ea 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -232,7 +232,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.section_context +val keep_hyps : env -> Id.Set.t -> Context.Named.t (** {5 Unsafe judgments. } We introduce here the pre-type of judgments, which is diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 2112284ea..81fd1427d 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -127,4 +127,4 @@ val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type (** Check that hyps are included in env and fails with error otherwise *) -val check_hyps_inclusion : env -> constr -> Context.section_context -> unit +val check_hyps_inclusion : env -> constr -> Context.Named.t -> unit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 666730e1a..9b0200039 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -130,8 +130,8 @@ val set_end_tac : Tacexpr.raw_tactic_expr -> unit (** [set_used_variables l] declares that section variables [l] will be used in the proof *) val set_used_variables : - Id.t list -> Context.section_context * (Loc.t * Names.Id.t) list -val get_used_variables : unit -> Context.section_context option + Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list +val get_used_variables : unit -> Context.Named.t option (** {6 Universe binders } *) val get_universe_binders : unit -> universe_binders option diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 4cb9f03ce..17cc92803 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -91,7 +91,7 @@ type pstate = { pid : Id.t; terminator : proof_terminator CEphemeron.key; endline_tactic : Tacexpr.raw_tactic_expr option; - section_vars : Context.section_context option; + section_vars : Context.Named.t option; proof : Proof.proof; strength : Decl_kinds.goal_kind; mode : proof_mode CEphemeron.key; diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli index 59daa2968..86fc1deff 100644 --- a/proofs/proof_global.mli +++ b/proofs/proof_global.mli @@ -143,8 +143,8 @@ val set_interp_tac : * (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.section_context * (Loc.t * Names.Id.t) list -val get_used_variables : unit -> Context.section_context option + Names.Id.t list -> Context.Named.t * (Loc.t * Names.Id.t) list +val get_used_variables : unit -> Context.Named.t option val get_universe_binders : unit -> universe_binders option |