diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/coqlib.ml | 2 | ||||
| -rw-r--r-- | library/coqlib.mli | 2 | ||||
| -rw-r--r-- | library/decl_kinds.ml | 8 | ||||
| -rw-r--r-- | library/declaremods.ml | 2 | ||||
| -rw-r--r-- | library/declaremods.mli | 2 | ||||
| -rw-r--r-- | library/decls.ml | 2 | ||||
| -rw-r--r-- | library/decls.mli | 2 | ||||
| -rw-r--r-- | library/global.ml | 13 | ||||
| -rw-r--r-- | library/global.mli | 11 | ||||
| -rw-r--r-- | library/globnames.ml | 2 | ||||
| -rw-r--r-- | library/globnames.mli | 2 | ||||
| -rw-r--r-- | library/goptions.ml | 2 | ||||
| -rw-r--r-- | library/goptions.mli | 2 | ||||
| -rw-r--r-- | library/keys.ml | 2 | ||||
| -rw-r--r-- | library/keys.mli | 2 | ||||
| -rw-r--r-- | library/kindops.ml | 2 | ||||
| -rw-r--r-- | library/kindops.mli | 2 | ||||
| -rw-r--r-- | library/lib.ml | 2 | ||||
| -rw-r--r-- | library/lib.mli | 2 | ||||
| -rw-r--r-- | library/libnames.ml | 2 | ||||
| -rw-r--r-- | library/libnames.mli | 2 | ||||
| -rw-r--r-- | library/libobject.ml | 2 | ||||
| -rw-r--r-- | library/libobject.mli | 2 | ||||
| -rw-r--r-- | library/library.ml | 31 | ||||
| -rw-r--r-- | library/library.mli | 7 | ||||
| -rw-r--r-- | library/nametab.ml | 2 | ||||
| -rw-r--r-- | library/nametab.mli | 2 | ||||
| -rw-r--r-- | library/states.ml | 2 | ||||
| -rw-r--r-- | library/states.mli | 2 | ||||
| -rw-r--r-- | library/summary.ml | 2 | ||||
| -rw-r--r-- | library/summary.mli | 2 |
31 files changed, 63 insertions, 59 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 8d5c2fb687..0e2ef95739 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 *) @@ -12,7 +12,9 @@ type discharge = DoDischarge | NoDischarge -type locality = Discharge | Local | Global +type import_status = ImportDefaultBehavior | ImportNeedQualified + +type locality = Discharge | Global of import_status type binding_kind = Explicit | Implicit @@ -46,7 +48,7 @@ type definition_object_kind = | Method | Let -type assumption_object_kind = Definitional | Logical | Conjectural +type assumption_object_kind = Definitional | Logical | Conjectural | Context (* [assumption_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 index b766b6e2cb..ef60a44ac7 100644 --- a/library/decls.ml +++ b/library/decls.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/decls.mli b/library/decls.mli index c0db537427..0d09499b51 100644 --- a/library/decls.mli +++ b/library/decls.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/global.ml b/library/global.ml index d5ffae7716..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 *) @@ -94,7 +94,7 @@ let make_sprop_cumulative () = globalize0 Safe_typing.make_sprop_cumulative let set_allow_sprop b = globalize0 (Safe_typing.set_allow_sprop b) let sprop_allowed () = Environ.sprop_allowed (env()) let export_private_constants ~in_section cd = globalize (Safe_typing.export_private_constants ~in_section cd) -let add_constant ?role ~in_section id d = globalize (Safe_typing.add_constant ?role ~in_section (i2l id) d) +let add_constant ~side_effect ~in_section id d = globalize (Safe_typing.add_constant ~side_effect ~in_section (i2l id) d) let add_recipe ~in_section id d = globalize (Safe_typing.add_recipe ~in_section (i2l id) d) let add_mind id mie = globalize (Safe_typing.add_mind (i2l id) mie) let add_modtype id me inl = globalize (Safe_typing.add_modtype (i2l id) me inl) @@ -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 eaa76c3117..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 *) @@ -46,7 +46,7 @@ val export_private_constants : in_section:bool -> Constr.constr Univ.in_universe_context_set * Safe_typing.exported_private_constant list val add_constant : - ?role:Entries.side_effect_role -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * Safe_typing.private_constants + side_effect:'a Safe_typing.effect_entry -> in_section:bool -> Id.t -> Safe_typing.global_declaration -> Constant.t * 'a val add_recipe : in_section:bool -> Id.t -> Cooking.recipe -> Constant.t val add_mind : Id.t -> Entries.mutual_inductive_entry -> MutInd.t @@ -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 2798c21c81..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 *) diff --git a/library/goptions.mli b/library/goptions.mli index ba86cb66ba..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 *) 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 index 247319fa2f..0bf55c62a9 100644 --- a/library/kindops.ml +++ b/library/kindops.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/kindops.mli b/library/kindops.mli index df39019da4..3c9f2bb7c3 100644 --- a/library/kindops.mli +++ b/library/kindops.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/lib.ml b/library/lib.ml index daa41eca65..ae657dbd70 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 *) diff --git a/library/lib.mli b/library/lib.mli index c19c3bf7fa..f6bd61e2da 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 *) 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 e3b8511af1..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 *) @@ -276,11 +276,11 @@ let in_import_library : DirPath.t list * bool -> obj = (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of 'a option array delayed - | Fetched of 'a option array + | ToFetch of 'a array delayed + | Fetched of 'a array let opaque_tables = - ref (LibraryMap.empty : (Constr.constr 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 @@ -310,6 +310,7 @@ let access_opaque_table dp i = let indirect_accessor = { Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_discharge = Cooking.cook_constr; } (************************************************************************) @@ -319,8 +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_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr option array +type seg_proofs = Opaqueproof.opaque_proofterm array let mk_library sd md digests univs = { @@ -344,7 +344,6 @@ let intern_from_file f = let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in let _ = System.skip_in_segment f ch in - let _ = System.skip_in_segment f ch in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in close_in ch; register_library_filename lsd.md_name f; @@ -527,15 +526,13 @@ let load_library_todo f = let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in - let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in let tasks, _, _ = System.marshal_in_segment f ch in - let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in + let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); - if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + s0, s1, Option.get s2, Option.get tasks, s4 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -578,10 +575,10 @@ let save_library_to ?todo ~output_native_objects dir f otab = List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e) Future.UUIDSet.empty l in let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in - let opaque_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in - let tasks, utab, dtab = + let opaque_table, f2t_map = Opaqueproof.dump ~except otab in + let tasks, utab = match todo with - | None -> None, None, None + | None -> None, None | Some (tasks, rcbackup) -> let tasks = List.map Stateid.(fun (r,b) -> @@ -589,8 +586,8 @@ let save_library_to ?todo ~output_native_objects dir f otab = with Not_found -> assert b; { r with uuid = -1 }, b) tasks in Some (tasks,rcbackup), - Some (Univ.ContextSet.empty,false), - Some disch_table in + Some (Univ.ContextSet.empty,false) + in let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); @@ -610,7 +607,6 @@ let save_library_to ?todo ~output_native_objects dir f otab = System.marshal_out_segment f' ch (sd : seg_sum); System.marshal_out_segment f' ch (md : seg_lib); System.marshal_out_segment f' ch (utab : seg_univ option); - System.marshal_out_segment f' ch (dtab : seg_discharge option); System.marshal_out_segment f' ch (tasks : 'tasks option); System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; @@ -630,7 +626,6 @@ let save_library_raw f sum lib univs proofs = System.marshal_out_segment f ch (sum : seg_sum); System.marshal_out_segment f ch (lib : seg_lib); System.marshal_out_segment f ch (Some univs : seg_univ option); - System.marshal_out_segment f ch (None : seg_discharge option); System.marshal_out_segment f ch (None : 'tasks option); System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch diff --git a/library/library.mli b/library/library.mli index 142206e2c5..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,8 +35,7 @@ type seg_sum type seg_lib type seg_univ = (* all_cst, finished? *) Univ.ContextSet.t * bool -type seg_discharge = Opaqueproof.cooking_info list array -type seg_proofs = Constr.constr 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 *) @@ -51,7 +50,7 @@ val save_library_to : val load_library_todo : CUnix.physical_path - -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit 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 *) |