aboutsummaryrefslogtreecommitdiff
path: root/library
diff options
context:
space:
mode:
Diffstat (limited to 'library')
-rw-r--r--library/coqlib.ml2
-rw-r--r--library/coqlib.mli2
-rw-r--r--library/decl_kinds.ml69
-rw-r--r--library/declaremods.ml2
-rw-r--r--library/declaremods.mli2
-rw-r--r--library/decls.ml46
-rw-r--r--library/decls.mli36
-rw-r--r--library/global.ml11
-rw-r--r--library/global.mli9
-rw-r--r--library/globnames.ml2
-rw-r--r--library/globnames.mli2
-rw-r--r--library/goptions.ml21
-rw-r--r--library/goptions.mli30
-rw-r--r--library/keys.ml2
-rw-r--r--library/keys.mli2
-rw-r--r--library/kindops.ml37
-rw-r--r--library/kindops.mli17
-rw-r--r--library/lib.ml32
-rw-r--r--library/lib.mli10
-rw-r--r--library/libnames.ml2
-rw-r--r--library/libnames.mli2
-rw-r--r--library/libobject.ml2
-rw-r--r--library/libobject.mli2
-rw-r--r--library/library.ml11
-rw-r--r--library/library.mli4
-rw-r--r--library/library.mllib3
-rw-r--r--library/nametab.ml2
-rw-r--r--library/nametab.mli2
-rw-r--r--library/states.ml2
-rw-r--r--library/states.mli2
-rw-r--r--library/summary.ml2
-rw-r--r--library/summary.mli2
32 files changed, 88 insertions, 284 deletions
diff --git a/library/coqlib.ml b/library/coqlib.ml
index 784360dc8a..7cd2e50274 100644
--- a/library/coqlib.ml
+++ b/library/coqlib.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/coqlib.mli b/library/coqlib.mli
index f6779dbbde..ab8b18c4fb 100644
--- a/library/coqlib.mli
+++ b/library/coqlib.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml
index 39042e1ab7..17746645ee 100644
--- a/library/decl_kinds.ml
+++ b/library/decl_kinds.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -8,71 +8,4 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-(** Informal mathematical status of declarations *)
-
-type discharge = DoDischarge | NoDischarge
-
-type import_status = ImportDefaultBehavior | ImportNeedQualified
-
-type locality = Discharge | Global of import_status
-
type binding_kind = Explicit | Implicit
-
-type polymorphic = bool
-
-type private_flag = bool
-
-type cumulative_inductive_flag = bool
-
-type theorem_kind =
- | Theorem
- | Lemma
- | Fact
- | Remark
- | Property
- | Proposition
- | Corollary
-
-type definition_object_kind =
- | Definition
- | Coercion
- | SubClass
- | CanonicalStructure
- | Example
- | Fixpoint
- | CoFixpoint
- | Scheme
- | StructureComponent
- | IdentityCoercion
- | Instance
- | Method
- | Let
-
-type assumption_object_kind = Definitional | Logical | Conjectural | Context
-
-(* [assumption_kind]
-
- | Local | Global
- ------------------------------------
- Definitional | Variable | Parameter
- Logical | Hypothesis | Axiom
-
-*)
-type assumption_kind = locality * polymorphic * assumption_object_kind
-type definition_kind = locality * polymorphic * definition_object_kind
-
-(** Kinds used in proofs *)
-
-type goal_object_kind =
- | DefinitionBody of definition_object_kind
- | Proof of theorem_kind
-
-type goal_kind = locality * polymorphic * goal_object_kind
-
-(** Kinds used in library *)
-
-type logical_kind =
- | IsPrimitive
- | IsAssumption of assumption_object_kind
- | IsDefinition of definition_object_kind
- | IsProof of theorem_kind
diff --git a/library/declaremods.ml b/library/declaremods.ml
index d74bdd484c..fc3e667c20 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 2b28ba908e..93aadd25de 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/decls.ml b/library/decls.ml
deleted file mode 100644
index b766b6e2cb..0000000000
--- a/library/decls.ml
+++ /dev/null
@@ -1,46 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-(** This module registers tables for some non-logical informations
- associated declarations *)
-
-open Names
-open Decl_kinds
-open Libnames
-
-(** Datas associated to section variables and local definitions *)
-
-type variable_data =
- DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
-
-let vartab =
- Summary.ref (Id.Map.empty : variable_data Id.Map.t) ~name:"VARIABLE"
-
-let add_variable_data id o = vartab := Id.Map.add id o !vartab
-
-let variable_path id = let (p,_,_,_,_) = Id.Map.find id !vartab in p
-let variable_opacity id = let (_,opaq,_,_,_) = Id.Map.find id !vartab in opaq
-let variable_kind id = let (_,_,_,_,k) = Id.Map.find id !vartab in k
-let variable_context id = let (_,_,ctx,_,_) = Id.Map.find id !vartab in ctx
-let variable_polymorphic id = let (_,_,_,p,_) = Id.Map.find id !vartab in p
-
-let variable_secpath id =
- let dir = drop_dirpath_prefix (Lib.library_dp()) (variable_path id) in
- make_qualid dir id
-
-let variable_exists id = Id.Map.mem id !vartab
-
-(** Datas associated to global parameters and constants *)
-
-let csttab = Summary.ref (Cmap.empty : logical_kind Cmap.t) ~name:"CONSTANT"
-
-let add_constant_kind kn k = csttab := Cmap.add kn k !csttab
-
-let constant_kind kn = Cmap.find kn !csttab
diff --git a/library/decls.mli b/library/decls.mli
deleted file mode 100644
index c0db537427..0000000000
--- a/library/decls.mli
+++ /dev/null
@@ -1,36 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Names
-open Libnames
-open Decl_kinds
-
-(** This module manages non-kernel informations about declarations. It
- is either non-logical informations or logical informations that
- have no place to be (yet) in the kernel *)
-
-(** Registration and access to the table of variable *)
-
-type variable_data =
- DirPath.t * bool (* opacity *) * Univ.ContextSet.t * polymorphic * logical_kind
-
-val add_variable_data : variable -> variable_data -> unit
-val variable_path : variable -> DirPath.t
-val variable_secpath : variable -> qualid
-val variable_kind : variable -> logical_kind
-val variable_opacity : variable -> bool
-val variable_context : variable -> Univ.ContextSet.t
-val variable_polymorphic : variable -> polymorphic
-val variable_exists : variable -> bool
-
-(** Registration and access to the table of constants *)
-
-val add_constant_kind : Constant.t -> logical_kind -> unit
-val constant_kind : Constant.t -> logical_kind
diff --git a/library/global.ml b/library/global.ml
index 3f30a63808..ca774dbd74 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -139,9 +139,14 @@ let body_of_constant_body access env cb =
| Undef _ | Primitive _ ->
None
| Def c ->
- Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+ let u = match cb.const_universes with
+ | Monomorphic _ -> Opaqueproof.PrivateMonomorphic ()
+ | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty)
+ in
+ Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb)
| OpaqueDef o ->
- Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
+ let c, u = Opaqueproof.force_proof access otab o in
+ Some (c, u, Declareops.constant_polymorphic_context cb)
let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
diff --git a/library/global.mli b/library/global.mli
index c36cec3511..51307b3604 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -100,13 +100,16 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
val opaque_tables : unit -> Opaqueproof.opaquetab
-val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t ->
+ (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
(** Returns the body of the constant if it has any, and the polymorphic context
it lives in. For monomorphic constant, the latter is empty, and for
polymorphic constants, the term contains De Bruijn universe variables that
need to be instantiated. *)
-val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.indirect_accessor ->
+ Opaqueproof.opaque Declarations.constant_body ->
+ (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
(** {6 Compiled libraries } *)
diff --git a/library/globnames.ml b/library/globnames.ml
index 99dcc43ad1..71447c4b81 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/globnames.mli b/library/globnames.mli
index 14e422b743..547755b088 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/goptions.ml b/library/goptions.ml
index f4b8ce9465..c7024ca81d 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -53,9 +53,9 @@ module MakeTable =
functor
(A : sig
type t
- type key
- val compare : t -> t -> int
- val table : (string * key table_of_A) list ref
+ type key
+ module Set : CSig.SetS with type elt = t
+ val table : (string * key table_of_A) list ref
val encode : Environ.env -> key -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
@@ -74,7 +74,7 @@ module MakeTable =
if String.List.mem_assoc nick !A.table then
user_err Pp.(str "Sorry, this table name (" ++ str nick ++ str ") is already used.")
- module MySet = Set.Make (struct type t = A.t let compare = A.compare end)
+ module MySet = A.Set
let t = Summary.ref MySet.empty ~name:nick
@@ -119,8 +119,9 @@ module MakeTable =
}
let _ = A.table := (nick, table_of_A)::!A.table
- let active c = MySet.mem c !t
- let elements () = MySet.elements !t
+
+ let v () = !t
+ let active x = A.Set.mem x !t
end
let string_table = ref []
@@ -138,7 +139,7 @@ module StringConvert = functor (A : StringConvertArg) ->
struct
type t = string
type key = string
- let compare = String.compare
+ module Set = CString.Set
let table = string_table
let encode _env x = x
let subst _ x = x
@@ -158,7 +159,7 @@ let get_ref_table k = String.List.assoc (nickname k) !ref_table
module type RefConvertArg =
sig
type t
- val compare : t -> t -> int
+ module Set : CSig.SetS with type elt = t
val encode : Environ.env -> qualid -> t
val subst : substitution -> t -> t
val printer : t -> Pp.t
@@ -171,7 +172,7 @@ module RefConvert = functor (A : RefConvertArg) ->
struct
type t = A.t
type key = qualid
- let compare = A.compare
+ module Set = A.Set
let table = ref_table
let encode = A.encode
let subst = A.subst
diff --git a/library/goptions.mli b/library/goptions.mli
index 381ba4d34a..29af196654 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -70,8 +70,8 @@ module MakeStringTable :
val member_message : string -> bool -> Pp.t
end) ->
sig
+ val v : unit -> CString.Set.t
val active : string -> bool
- val elements : unit -> string list
end
(** The functor [MakeRefTable] declares a new table of objects of type
@@ -87,19 +87,19 @@ end
module MakeRefTable :
functor
(A : sig
- type t
- val compare : t -> t -> int
- val encode : Environ.env -> qualid -> t
- val subst : substitution -> t -> t
- val printer : t -> Pp.t
- val key : option_name
- val title : string
- val member_message : t -> bool -> Pp.t
- end) ->
- sig
- val active : A.t -> bool
- val elements : unit -> A.t list
- end
+ type t
+ module Set : CSig.SetS with type elt = t
+ val encode : Environ.env -> qualid -> t
+ val subst : substitution -> t -> t
+ val printer : t -> Pp.t
+ val key : option_name
+ val title : string
+ val member_message : t -> bool -> Pp.t
+ end) ->
+sig
+ val v : unit -> A.Set.t
+ val active : A.t -> bool
+end
(** {6 Options. } *)
diff --git a/library/keys.ml b/library/keys.ml
index 45b6fae2f0..30ecc9dfdb 100644
--- a/library/keys.ml
+++ b/library/keys.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/keys.mli b/library/keys.mli
index 198383650a..a7adf7791b 100644
--- a/library/keys.mli
+++ b/library/keys.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/kindops.ml b/library/kindops.ml
deleted file mode 100644
index 247319fa2f..0000000000
--- a/library/kindops.ml
+++ /dev/null
@@ -1,37 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Decl_kinds
-
-(** Operations about types defined in [Decl_kinds] *)
-
-let logical_kind_of_goal_kind = function
- | DefinitionBody d -> IsDefinition d
- | Proof s -> IsProof s
-
-let string_of_theorem_kind = function
- | Theorem -> "Theorem"
- | Lemma -> "Lemma"
- | Fact -> "Fact"
- | Remark -> "Remark"
- | Property -> "Property"
- | Proposition -> "Proposition"
- | Corollary -> "Corollary"
-
-let string_of_definition_object_kind = function
- | Definition -> "Definition"
- | Example -> "Example"
- | Coercion -> "Coercion"
- | SubClass -> "SubClass"
- | CanonicalStructure -> "Canonical Structure"
- | Instance -> "Instance"
- | Let -> "Let"
- | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) ->
- CErrors.anomaly (Pp.str "Internal definition kind.")
diff --git a/library/kindops.mli b/library/kindops.mli
deleted file mode 100644
index df39019da4..0000000000
--- a/library/kindops.mli
+++ /dev/null
@@ -1,17 +0,0 @@
-(************************************************************************)
-(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
-(* <O___,, * (see CREDITS file for the list of authors) *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(* * (see LICENSE file for the text of the license) *)
-(************************************************************************)
-
-open Decl_kinds
-
-(** Operations about types defined in [Decl_kinds] *)
-
-val logical_kind_of_goal_kind : goal_object_kind -> logical_kind
-val string_of_theorem_kind : theorem_kind -> string
-val string_of_definition_object_kind : definition_object_kind -> string
diff --git a/library/lib.ml b/library/lib.ml
index daa41eca65..3eb74808e4 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -411,8 +411,12 @@ type abstr_info = {
type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
type secentry =
- | Variable of (Names.Id.t * Decl_kinds.binding_kind *
- Decl_kinds.polymorphic * Univ.ContextSet.t)
+ | Variable of {
+ id:Names.Id.t;
+ kind:Decl_kinds.binding_kind;
+ poly:bool;
+ univs:Univ.ContextSet.t;
+ }
| Context of Univ.ContextSet.t
let sectab =
@@ -424,16 +428,16 @@ let add_section () =
(Names.Cmap.empty,Names.Mindmap.empty)) :: !sectab
let check_same_poly p vars =
- let pred = function Context _ -> p = false | Variable (_, _, poly, _) -> p != poly in
+ let pred = function Context _ -> p = false | Variable {poly} -> p != poly in
if List.exists pred vars then
user_err Pp.(str "Cannot mix universe polymorphic and monomorphic declarations in sections.")
-let add_section_variable id impl poly ctx =
+let add_section_variable ~name ~kind ~poly univs =
match !sectab with
| [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
| (vars,repl,abs)::sl ->
List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
- sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
+ sectab := (Variable {id=name;kind;poly;univs}::vars,repl,abs)::sl
let add_section_context ctx =
match !sectab with
@@ -448,7 +452,7 @@ let is_polymorphic_univ u =
let open Univ in
List.iter (fun (vars,_,_) ->
List.iter (function
- | Variable (_,_,poly,(univs,_)) ->
+ | Variable {poly;univs=(univs,_)} ->
if LSet.mem u univs then raise (PolyFound poly)
| Context (univs,_) ->
if LSet.mem u univs then raise (PolyFound true)
@@ -459,12 +463,12 @@ let is_polymorphic_univ u =
let extract_hyps (secs,ohyps) =
let rec aux = function
- | (Variable (id,impl,poly,ctx)::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
+ | (Variable {id;kind;poly;univs}::idl, decl::hyps) when Names.Id.equal id (NamedDecl.get_id decl) ->
let l, r = aux (idl,hyps) in
- (decl,impl) :: l, if poly then Univ.ContextSet.union r ctx else r
- | (Variable (_,_,poly,ctx)::idl,hyps) ->
+ (decl,kind) :: l, if poly then Univ.ContextSet.union r univs else r
+ | (Variable {poly;univs}::idl,hyps) ->
let l, r = aux (idl,hyps) in
- l, if poly then Univ.ContextSet.union r ctx else r
+ l, if poly then Univ.ContextSet.union r univs else r
| (Context ctx :: idl, hyps) ->
let l, r = aux (idl, hyps) in
l, Univ.ContextSet.union r ctx
@@ -509,11 +513,11 @@ let add_section_replacement f g poly hyps =
} in
sectab := (vars,f (inst,args) exps, g info abs) :: sl
-let add_section_kn poly kn =
+let add_section_kn ~poly kn =
let f x (l1,l2) = (l1,Names.Mindmap.add kn x l2) in
add_section_replacement f f poly
-let add_section_constant poly kn =
+let add_section_constant ~poly kn =
let f x (l1,l2) = (Names.Cmap.add kn x l1,l2) in
add_section_replacement f f poly
@@ -543,7 +547,7 @@ let variable_section_segment_of_reference gr =
let section_instance = function
| VarRef id ->
let eq = function
- | Variable (id',_,_,_) -> Names.Id.equal id id'
+ | Variable {id=id'} -> Names.Id.equal id id'
| Context _ -> false
in
if List.exists eq (pi1 (List.hd !sectab))
diff --git a/library/lib.mli b/library/lib.mli
index c19c3bf7fa..2cd43b66b3 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -178,12 +178,10 @@ val variable_section_segment_of_reference : GlobRef.t -> variable_context
val section_instance : GlobRef.t -> Univ.Instance.t * Id.t array
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_variable : name:Id.t -> kind:Decl_kinds.binding_kind -> poly:bool -> Univ.ContextSet.t -> unit
val add_section_context : Univ.ContextSet.t -> unit
-val add_section_constant : Decl_kinds.polymorphic ->
- Constant.t -> Constr.named_context -> unit
-val add_section_kn : Decl_kinds.polymorphic ->
- MutInd.t -> Constr.named_context -> unit
+val add_section_constant : poly:bool -> Constant.t -> Constr.named_context -> unit
+val add_section_kn : poly:bool -> MutInd.t -> Constr.named_context -> unit
val replacement_context : unit -> Opaqueproof.work_list
val is_polymorphic_univ : Univ.Level.t -> bool
diff --git a/library/libnames.ml b/library/libnames.ml
index 41b38e0378..18af216e46 100644
--- a/library/libnames.ml
+++ b/library/libnames.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/libnames.mli b/library/libnames.mli
index 7d77d95991..4455e29818 100644
--- a/library/libnames.mli
+++ b/library/libnames.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/libobject.ml b/library/libobject.ml
index 3d17b4a605..72791661bc 100644
--- a/library/libobject.ml
+++ b/library/libobject.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/libobject.mli b/library/libobject.mli
index 00515bd273..a7151d3bf2 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/library.ml b/library/library.ml
index 1ac75d2fdc..0d4148d7e4 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -280,7 +280,7 @@ type 'a table_status =
| Fetched of 'a array
let opaque_tables =
- ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t)
+ ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t)
let add_opaque_table dp st =
opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -306,10 +306,7 @@ let access_table what tables dp i =
let access_opaque_table dp i =
let what = "opaque proofs" in
- let (info, n, c) = access_table what opaque_tables dp i in
- match c with
- | None -> None
- | Some c -> Some (Cooking.cook_constr info n c)
+ access_table what opaque_tables dp i
let indirect_accessor = {
Opaqueproof.access_proof = access_opaque_table;
@@ -323,7 +320,7 @@ type seg_sum = summary_disk
type seg_lib = library_disk
type seg_univ = (* true = vivo, false = vi *)
Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
let mk_library sd md digests univs =
{
diff --git a/library/library.mli b/library/library.mli
index 727eca10cf..bb6c42e393 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
@@ -35,7 +35,7 @@ type seg_sum
type seg_lib
type seg_univ = (* all_cst, finished? *)
Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
(** Open a module (or a library); if the boolean is true then it's also
an export otherwise just a simple import *)
diff --git a/library/library.mllib b/library/library.mllib
index ef53471377..35af5fa43b 100644
--- a/library/library.mllib
+++ b/library/library.mllib
@@ -1,16 +1,15 @@
+Decl_kinds
Libnames
Globnames
Libobject
Summary
Nametab
Global
-Decl_kinds
Lib
Declaremods
Library
States
Kindops
Goptions
-Decls
Keys
Coqlib
diff --git a/library/nametab.ml b/library/nametab.ml
index bd0ea5f04f..71ee7a6d5a 100644
--- a/library/nametab.ml
+++ b/library/nametab.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/nametab.mli b/library/nametab.mli
index 33cb4faf99..6ee22fc283 100644
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/states.ml b/library/states.ml
index 92bdc410a3..a73f16957d 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/states.mli b/library/states.mli
index 52feb95222..c4f3eae49d 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/summary.ml b/library/summary.ml
index 8fbca44353..b3ec4c2db2 100644
--- a/library/summary.ml
+++ b/library/summary.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
diff --git a/library/summary.mli b/library/summary.mli
index 3875bcfe9e..3a122edf3d 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
-(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *)
+(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *)
(* <O___,, * (see CREDITS file for the list of authors) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 00:01:11 +0000