diff options
Diffstat (limited to 'kernel')
95 files changed, 262 insertions, 225 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index fc7d1a54f2..6be8a59aeb 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.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/kernel/cClosure.mli b/kernel/cClosure.mli index 60185464c5..027d5245c9 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.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/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index fdc93cfa89..d854cadd15 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.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/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 3f8174bd7b..6913371caf 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.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/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index 7570004fe5..009db05ea2 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.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/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 423e7bbe65..06b380ef89 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.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/kernel/cbytegen.ml b/kernel/cbytegen.ml index 90fbcb8ae3..83d2a58d83 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.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/kernel/cbytegen.mli b/kernel/cbytegen.mli index bdaf5fe422..814902a554 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.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/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index a84a7c0cf9..76e2515ea7 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.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/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 41cc641dc8..9184164504 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Vmvalues diff --git a/kernel/constr.ml b/kernel/constr.ml index d74c96af84..8375316003 100644 --- a/kernel/constr.ml +++ b/kernel/constr.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/kernel/constr.mli b/kernel/constr.mli index aa5878c9d7..45ec8a7e64 100644 --- a/kernel/constr.mli +++ b/kernel/constr.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/kernel/context.ml b/kernel/context.ml index 290e85294b..2ef750ad69 100644 --- a/kernel/context.ml +++ b/kernel/context.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/kernel/context.mli b/kernel/context.mli index 7b67e54ba4..8f233613da 100644 --- a/kernel/context.mli +++ b/kernel/context.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/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index fe82353b70..7ce320381c 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.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/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index bc06cc21b6..918dc8c928 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.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/kernel/cooking.ml b/kernel/cooking.ml index 1336e3e8bf..0951b07d49 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.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 *) @@ -159,7 +159,6 @@ type 'opaque result = { cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; - cook_private_univs : Univ.ContextSet.t option; cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; @@ -202,21 +201,30 @@ let lift_univs cb subst auctx0 = let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in subst, (Polymorphic auctx) -let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) = +let cook_constr { Opaqueproof.modlist ; abstract } (c, priv) = let cache = RefTable.create 13 in let abstract, usubst, abs_ctx = abstract in - let ainst = Instance.of_array (Array.init univs Level.var) in - let usubst = Instance.append usubst ainst in + let usubst, priv = match priv with + | Opaqueproof.PrivateMonomorphic () -> + let () = assert (AUContext.is_empty abs_ctx) in + let () = assert (Instance.is_empty usubst) in + usubst, priv + | Opaqueproof.PrivatePolymorphic (univs, ctx) -> + let ainst = Instance.of_array (Array.init univs Level.var) in + let usubst = Instance.append usubst ainst in + let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in + let univs = univs + AUContext.size abs_ctx in + usubst, Opaqueproof.PrivatePolymorphic (univs, ctx) + in let expmod = expmod_constr_subst cache modlist usubst in let hyps = Context.Named.map expmod abstract in let hyps = abstract_context hyps in let c = abstract_constant_body (expmod c) hyps in - univs + AUContext.size abs_ctx, c + (c, priv) -let cook_constr infos univs c = - let fold info (univs, c) = cook_constr info (univs, c) in - let (_, c) = List.fold_right fold infos (univs, c) in - c +let cook_constr infos c = + let fold info c = cook_constr info c in + List.fold_right fold infos c let cook_constant { from = cb; info } = let { Opaqueproof.modlist; abstract } = info in @@ -240,15 +248,10 @@ let cook_constant { from = cb; info } = hyps) hyps0 ~init:cb.const_hyps in let typ = abstract_constant_type (expmod cb.const_type) hyps in - let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints - (Univ.make_instance_subst usubst))) - cb.const_private_poly_univs - in { cook_body = body; cook_type = typ; cook_universes = univs; - cook_private_univs = private_univs; cook_relevance = cb.const_relevance; cook_inline = cb.const_inline_code; cook_context = Some const_hyps; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 934b7c6b50..671cdf51fe 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.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 *) @@ -21,14 +21,14 @@ type 'opaque result = { cook_body : (constr Mod_subst.substituted, 'opaque) constant_def; cook_type : types; cook_universes : universes; - cook_private_univs : Univ.ContextSet.t option; cook_relevance : Sorts.relevance; cook_inline : inline; cook_context : Constr.named_context option; } val cook_constant : recipe -> Opaqueproof.opaque result -val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr +val cook_constr : Opaqueproof.cooking_info list -> + (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes) val cook_inductive : Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 8bef6aec42..6c9e73b50d 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.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/kernel/csymtable.mli b/kernel/csymtable.mli index 72c96b0b9f..3322c89aa9 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.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/kernel/declarations.ml b/kernel/declarations.ml index 388b4f14bf..dff19dee5e 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.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,6 @@ type 'opaque constant_body = { const_relevance : Sorts.relevance; const_body_code : Cemitcodes.to_patch_substituted option; const_universes : universes; - const_private_poly_univs : Univ.ContextSet.t option; const_inline_code : bool; const_typing_flags : typing_flags; (** The typing options which were used for diff --git a/kernel/declareops.ml b/kernel/declareops.ml index de9a052096..7a553700e8 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.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 *) @@ -113,7 +113,6 @@ let subst_const_body sub cb = const_body_code = Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code; const_universes = cb.const_universes; - const_private_poly_univs = cb.const_private_poly_univs; const_relevance = cb.const_relevance; const_inline_code = cb.const_inline_code; const_typing_flags = cb.const_typing_flags } @@ -144,16 +143,11 @@ let hcons_universes cbu = | Polymorphic ctx -> Polymorphic (Univ.hcons_abstract_universe_context ctx) -let hcons_const_private_univs = function - | None -> None - | Some univs -> Some (Univ.hcons_universe_context_set univs) - let hcons_const_body cb = { cb with const_body = hcons_const_def cb.const_body; const_type = Constr.hcons cb.const_type; const_universes = hcons_universes cb.const_universes; - const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs; } (** {6 Inductive types } *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index fb02c6a029..5a1331afa9 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.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/kernel/entries.ml b/kernel/entries.ml index 45b11e97ba..de1ce609fd 100644 --- a/kernel/entries.ml +++ b/kernel/entries.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/kernel/environ.ml b/kernel/environ.ml index c47bde0864..32f9069747 100644 --- a/kernel/environ.ml +++ b/kernel/environ.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/kernel/environ.mli b/kernel/environ.mli index 2abcea148a..a4cd576bcc 100644 --- a/kernel/environ.mli +++ b/kernel/environ.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/kernel/esubst.ml b/kernel/esubst.ml index 9fc3b11d78..f10cf20b42 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.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/kernel/esubst.mli b/kernel/esubst.mli index 475b64f472..400f91d302 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.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/kernel/evar.ml b/kernel/evar.ml index bbe143092b..a0bed31f68 100644 --- a/kernel/evar.ml +++ b/kernel/evar.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/kernel/evar.mli b/kernel/evar.mli index d14cdce27a..25a92d3e1d 100644 --- a/kernel/evar.mli +++ b/kernel/evar.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/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 6564954dfd..a8a4ffce9c 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.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/kernel/indTyping.ml b/kernel/indTyping.ml index 65298938fa..c8e04b9fee 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.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/kernel/indTyping.mli b/kernel/indTyping.mli index ef2c30b76a..aaa0d6a149 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.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/kernel/indtypes.ml b/kernel/indtypes.ml index bb3b0a538e..b0366d6ec0 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.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/kernel/indtypes.mli b/kernel/indtypes.mli index 1b8e4208ff..240ba4e2bb 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.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/kernel/inductive.ml b/kernel/inductive.ml index beff8f4421..cd969ea457 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.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/kernel/inductive.mli b/kernel/inductive.mli index f705cdf646..8c40c318c5 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.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/kernel/mod_subst.ml b/kernel/mod_subst.ml index 9397772415..c5ea32e157 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.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/kernel/mod_subst.mli b/kernel/mod_subst.mli index 8ab3d04402..b69e62b8a6 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.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/kernel/mod_typing.ml b/kernel/mod_typing.ml index 72393d0081..9305a91731 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.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/kernel/mod_typing.mli b/kernel/mod_typing.mli index e74f455efe..aa8aa96746 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.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/kernel/modops.ml b/kernel/modops.ml index 472fddb829..4808ed14e4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.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 *) @@ -329,7 +329,6 @@ let strengthen_const mp_from l cb resolver = let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in { cb with const_body = Def (Mod_subst.from_val (mkConstU (con,u))); - const_private_poly_univs = None; const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) } let rec strengthen_mod mp_from mp_to mb = diff --git a/kernel/modops.mli b/kernel/modops.mli index 119ce2b359..badbd973ae 100644 --- a/kernel/modops.mli +++ b/kernel/modops.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/kernel/names.ml b/kernel/names.ml index 047a1d6525..655bf50087 100644 --- a/kernel/names.ml +++ b/kernel/names.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/kernel/names.mli b/kernel/names.mli index 2238e932b0..44e8dd4a83 100644 --- a/kernel/names.mli +++ b/kernel/names.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/kernel/nativecode.ml b/kernel/nativecode.ml index 3f791dfc22..fc9e69d9e3 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.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/kernel/nativecode.mli b/kernel/nativecode.mli index b5c03b6ca3..955c4ad899 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.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/kernel/nativeconv.ml b/kernel/nativeconv.ml index d153f84e9c..a98523ba66 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.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/kernel/nativeconv.mli b/kernel/nativeconv.mli index 2111739d5e..9cacf0f4ef 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.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/kernel/nativelambda.ml b/kernel/nativelambda.ml index 62afd9df68..70b3beb2dc 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.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/kernel/nativelambda.mli b/kernel/nativelambda.mli index 446df1a1ea..f17339f84d 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.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/kernel/nativelib.ml b/kernel/nativelib.ml index 43c9676f05..94a8b1310a 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.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/kernel/nativelib.mli b/kernel/nativelib.mli index e113350368..194efecd9a 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.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/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 5d1b882361..1dbab6c690 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.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/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 31e5255fc4..168bf646af 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.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/kernel/nativevalues.ml b/kernel/nativevalues.ml index 3eb51ffc59..b3ad3949dc 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.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/kernel/nativevalues.mli b/kernel/nativevalues.mli index 58cb6e2c30..b5b4569a24 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.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/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index e18b726111..e256466112 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.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 *) @@ -20,18 +20,28 @@ type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } +type 'a delayed_universes = +| PrivateMonomorphic of 'a +| PrivatePolymorphic of int * Univ.ContextSet.t + +type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option + type indirect_accessor = { - access_proof : DirPath.t -> int -> constr option; - access_discharge : cooking_info list -> int -> constr -> constr; + access_proof : DirPath.t -> int -> opaque_proofterm; + access_discharge : cooking_info list -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } -type proofterm = (constr * Univ.ContextSet.t) Future.computation -type universes = int +let drop_mono = function +| PrivateMonomorphic _ -> PrivateMonomorphic () +| PrivatePolymorphic _ as ctx -> ctx + +type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation + type opaque = | Indirect of substitution list * DirPath.t * int (* subst, lib, index *) - | Direct of universes * cooking_info list * proofterm + | Direct of cooking_info list * proofterm type opaquetab = { - opaque_val : (int * cooking_info list * proofterm) Int.Map.t; + opaque_val : (cooking_info list * proofterm) Int.Map.t; (** Actual proof terms *) opaque_len : int; (** Size of the above map *) @@ -46,25 +56,28 @@ let empty_opaquetab = { let not_here () = CErrors.user_err Pp.(str "Cannot access opaque delayed proof") -let create ~univs cu = Direct (univs, [],cu) +let create cu = Direct ([],cu) let turn_indirect dp o tab = match o with | Indirect (_,_,i) -> if not (Int.Map.mem i tab.opaque_val) then CErrors.anomaly (Pp.str "Indirect in a different table.") else CErrors.anomaly (Pp.str "Already an indirect opaque.") - | Direct (nunivs, d, cu) -> + | Direct (d, cu) -> (* Invariant: direct opaques only exist inside sections, we turn them indirect as soon as we are at toplevel. At this moment, we perform hashconsing of their contents, potentially as a future. *) let hcons (c, u) = let c = Constr.hcons c in - let u = Univ.hcons_universe_context_set u in + let u = match u with + | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u) + | PrivatePolymorphic (n, u) -> PrivatePolymorphic (n, Univ.hcons_universe_context_set u) + in (c, u) in let cu = Future.chain cu hcons in let id = tab.opaque_len in - let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in + let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in let opaque_dir = if DirPath.equal dp tab.opaque_dir then tab.opaque_dir else if DirPath.equal tab.opaque_dir DirPath.initial then dp @@ -79,8 +92,8 @@ let subst_opaque sub = function let discharge_direct_opaque ci = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") - | Direct (n, d, cu) -> - Direct (n, ci :: d, cu) + | Direct (d, cu) -> + Direct (ci :: d, cu) let join except cu = match except with | None -> ignore (Future.join cu) @@ -89,61 +102,70 @@ let join except cu = match except with else ignore (Future.join cu) let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,_,cu) -> join except cu + | Direct (_,cu) -> join except cu | Indirect (_,dp,i) -> if DirPath.equal dp odp then - let (_, _, fp) = Int.Map.find i prfs in + let (_, fp) = Int.Map.find i prfs in join except fp let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (n, d, cu) -> - let (c, _) = Future.force cu in - access.access_discharge d n c + | Direct (d, cu) -> + let (c, u) = Future.force cu in + access.access_discharge d (c, drop_mono u) | Indirect (l,dp,i) -> - let c = + let c, u = if DirPath.equal dp odp then - let (n, d, cu) = Int.Map.find i prfs in - let (c, _) = Future.force cu in - access.access_discharge d n c - else match access.access_proof dp i with - | None -> not_here () - | Some v -> v + let (d, cu) = Int.Map.find i prfs in + let (c, u) = Future.force cu in + access.access_discharge d (c, drop_mono u) + else + let (d, cu) = access.access_proof dp i in + match cu with + | None -> not_here () + | Some (c, u) -> access.access_discharge d (c, u) in - force_constr (List.fold_right subst_substituted l (from_val c)) + let c = force_constr (List.fold_right subst_substituted l (from_val c)) in + (c, u) + +let get_mono (_, u) = match u with +| PrivateMonomorphic ctx -> ctx +| PrivatePolymorphic _ -> Univ.ContextSet.empty let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function - | Direct (_,_,cu) -> - snd(Future.force cu) + | Direct (_,cu) -> + get_mono (Future.force cu) | Indirect (_,dp,i) -> if DirPath.equal dp odp then - let (_, _, cu) = Int.Map.find i prfs in - snd (Future.force cu) + let ( _, cu) = Int.Map.find i prfs in + get_mono (Future.force cu) else Univ.ContextSet.empty let get_direct_constraints = function | Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.") -| Direct (_, _, cu) -> Future.chain cu snd +| Direct (_, cu) -> + Future.chain cu get_mono module FMap = Future.UUIDMap let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } = - let opaque_table = Array.make n ([], 0, None) in + let opaque_table = Array.make n ([], None) in let f2t_map = ref FMap.empty in - let iter n (univs, d, cu) = + let iter n (d, cu) = let uid = Future.uuid cu in let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in let c = if Future.is_val cu then - let (c, _) = Future.force cu in - Some c + let (c, priv) = Future.force cu in + let priv = drop_mono priv in + Some (c, priv) else if Future.UUIDSet.mem uid except then None else CErrors.anomaly Pp.(str"Proof object "++int n++str" is not checked nor to be checked") in - opaque_table.(n) <- (d, univs, c) + opaque_table.(n) <- (d, c) in let () = Int.Map.iter iter otab in opaque_table, !f2t_map diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 6e275649cd..7c53656c3c 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.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 *) @@ -21,14 +21,19 @@ open Mod_subst When it is [turn_indirect] the data is relocated to an opaque table and the [opaque] is turned into an index. *) -type proofterm = (constr * Univ.ContextSet.t) Future.computation +type 'a delayed_universes = +| PrivateMonomorphic of 'a +| PrivatePolymorphic of int * Univ.ContextSet.t + (** Number of surrounding bound universes + local constraints *) + +type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation type opaquetab type opaque val empty_opaquetab : opaquetab (** From a [proofterm] to some [opaque]. *) -val create : univs:int -> proofterm -> opaque +val create : proofterm -> opaque (** Turn a direct [opaque] into an indirect one. It is your responsibility to hashcons the inner term beforehand. The integer is an hint of the maximum id @@ -42,9 +47,12 @@ type cooking_info = { modlist : work_list; abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t } +type opaque_proofterm = cooking_info list * (Constr.t * unit delayed_universes) option + type indirect_accessor = { - access_proof : DirPath.t -> int -> constr option; - access_discharge : cooking_info list -> int -> constr -> constr; + access_proof : DirPath.t -> int -> opaque_proofterm; + access_discharge : cooking_info list -> + (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes); } (** When stored indirectly, opaque terms are indexed by their library dirpath and an integer index. The two functions above activate @@ -53,7 +61,7 @@ type indirect_accessor = { (** From a [opaque] back to a [constr]. This might use the indirect opaque accessor given as an argument. *) -val force_proof : indirect_accessor -> opaquetab -> opaque -> constr +val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation @@ -65,5 +73,5 @@ val discharge_direct_opaque : val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit val dump : ?except:Future.UUIDSet.t -> opaquetab -> - (cooking_info list * int * Constr.t option) array * + opaque_proofterm array * int Future.UUIDMap.t diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 11ece78fe0..53f228c618 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.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/kernel/reduction.mli b/kernel/reduction.mli index 7dcafb7d7b..ab34d3a6dc 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.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/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index e1c4cec5b5..873c6af93d 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.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/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 09e8140308..2a7b390951 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.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/kernel/retypeops.ml b/kernel/retypeops.ml index 204dec3eda..a51b762f95 100644 --- a/kernel/retypeops.ml +++ b/kernel/retypeops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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 Util diff --git a/kernel/retypeops.mli b/kernel/retypeops.mli index f30c541c3f..f4497be44b 100644 --- a/kernel/retypeops.mli +++ b/kernel/retypeops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* 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 *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** We can take advantage of non-cumulativity of SProp to avoid fully diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 0b0f14eee7..a980d22e42 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.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 *) @@ -308,23 +308,24 @@ let env_of_safe_env senv = senv.env let env_of_senv = env_of_safe_env type constraints_addition = - | Now of bool * Univ.ContextSet.t + | Now of Univ.ContextSet.t | Later of Univ.ContextSet.t Future.computation +let push_context_set poly cst senv = + { senv with + env = Environ.push_context_set ~strict:(not poly) cst senv.env; + univ = Univ.ContextSet.union cst senv.univ } + let add_constraints cst senv = match cst with | Later fc -> {senv with future_cst = fc :: senv.future_cst} - | Now (poly,cst) -> - { senv with - env = Environ.push_context_set ~strict:(not poly) cst senv.env; - univ = Univ.ContextSet.union cst senv.univ } + | Now cst -> + push_context_set false cst senv let add_constraints_list cst senv = List.fold_left (fun acc c -> add_constraints c acc) senv cst -let push_context_set poly ctx = add_constraints (Now (poly,ctx)) - let is_curmod_library senv = match senv.modvariant with LIBRARY -> true | _ -> false @@ -333,7 +334,7 @@ let join_safe_environment ?(except=Future.UUIDSet.empty) e = List.fold_left (fun e fc -> if Future.UUIDSet.mem (Future.uuid fc) except then e - else add_constraints (Now (false, Future.join fc)) e) + else add_constraints (Now (Future.join fc)) e) {e with future_cst = []} e.future_cst let is_joined_environment e = List.is_empty e.future_cst @@ -456,22 +457,22 @@ let globalize_constant_universes cb = match cb.const_universes with | Monomorphic cstrs -> (* Constraints hidden in the opaque body are added by [add_constant_aux] *) - [Now (false, cstrs)] + [cstrs] | Polymorphic _ -> - [Now (true, Univ.ContextSet.empty)] + [] let globalize_mind_universes mb = match mb.mind_universes with | Monomorphic ctx -> - [Now (false, ctx)] - | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)] + [ctx] + | Polymorphic _ -> [] let constraints_of_sfb sfb = match sfb with | SFBconst cb -> globalize_constant_universes cb | SFBmind mib -> globalize_mind_universes mib - | SFBmodtype mtb -> [Now (false, mtb.mod_constraints)] - | SFBmodule mb -> [Now (false, mb.mod_constraints)] + | SFBmodtype mtb -> [mtb.mod_constraints] + | SFBmodule mb -> [mb.mod_constraints] let add_retroknowledge pttc senv = { senv with @@ -508,7 +509,7 @@ let add_field ?(is_include=false) ((l,sfb) as field) gn senv = else (* Delayed constraints from opaque body are added by [add_constant_aux] *) let cst = constraints_of_sfb sfb in - add_constraints_list cst senv + List.fold_left (fun senv cst -> push_context_set false cst senv) senv cst in let env' = match sfb, gn with | SFBconst cb, C con -> Environ.add_constant con cb senv.env @@ -544,7 +545,7 @@ let add_constant_aux ~in_section senv (kn, cb) = let fc = Opaqueproof.get_direct_constraints o in begin match Future.peek_val fc with | None -> [Later fc] - | Some c -> [Now (false, c)] + | Some c -> [Now c] end | Undef _ | Def _ | Primitive _ | OpaqueDef _ -> [] in @@ -725,11 +726,15 @@ let export_side_effects mb env (b_ctx, eff) = let kn = eff.seff_constant in let ce = constant_entry_of_side_effect eff in let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in - let map cu = + let map cu = let (c, u) = Future.force cu in - let () = assert (Univ.ContextSet.is_empty u) in + let () = match u with + | Opaqueproof.PrivateMonomorphic ctx + | Opaqueproof.PrivatePolymorphic (_, ctx) -> + assert (Univ.ContextSet.is_empty ctx) + in c - in + in let cb = map_constant map cb in let eff = { eff with seff_body = cb } in (push_seff env eff, export_eff eff) @@ -742,13 +747,16 @@ let export_side_effects mb env (b_ctx, eff) = in translate_seff trusted seff [] env -let n_univs cb = match cb.const_universes with -| Monomorphic _ -> 0 -| Polymorphic auctx -> Univ.AUContext.size auctx - let export_private_constants ~in_section ce senv = let exported, ce = export_side_effects senv.revstruct senv.env ce in - let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in + let map univs p = + let local = match univs with + | Monomorphic _ -> Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty + | Polymorphic auctx -> Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, Univ.ContextSet.empty) + in + Opaqueproof.create (Future.from_val (p, local)) + in + let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in let bodies = List.map map exported in let exported = List.map (fun (kn, _) -> kn) exported in let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in @@ -775,7 +783,7 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen Term_typing.translate_constant Term_typing.Pure senv.env kn ce in let senv = - let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in + let cb = map_constant (fun c -> Opaqueproof.create c) cb in add_constant_aux ~in_section senv (kn, cb) in let senv = match decl with @@ -791,14 +799,16 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen | (Primitive _ | Undef _) -> assert false | Def c -> (Def c, cb.const_universes) | OpaqueDef o -> - let (b, ctx) = Future.force o in - match cb.const_universes with - | Monomorphic ctx' -> + let (b, delayed) = Future.force o in + match cb.const_universes, delayed with + | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx -> OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx') - | Polymorphic auctx -> + | Polymorphic auctx, Opaqueproof.PrivatePolymorphic (_, ctx) -> (* Upper layers enforce that there are no internal constraints *) let () = assert (Univ.ContextSet.is_empty ctx) in OpaqueDef b, Polymorphic auctx + | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) -> + assert false in let cb = { cb with const_body = body; const_universes = univs } in let from_env = CEphemeron.create senv.revstruct in @@ -842,13 +852,13 @@ let add_modtype l params_mte inl senv = (** full_add_module adds module with universes and constraints *) let full_add_module mb senv = - let senv = add_constraints (Now (false, mb.mod_constraints)) senv in + let senv = add_constraints (Now mb.mod_constraints) senv in let dp = ModPath.dp mb.mod_mp in let linkinfo = Nativecode.link_info_of_dirpath dp in { senv with env = Modops.add_linked_module mb linkinfo senv.env } let full_add_module_type mp mt senv = - let senv = add_constraints (Now (false, mt.mod_constraints)) senv in + let senv = add_constraints (Now mt.mod_constraints) senv in { senv with env = Modops.add_module_type mp mt senv.env } (** Insertion of modules *) @@ -1028,7 +1038,7 @@ let add_include me is_module inl senv = let sign,(),resolver,cst = translate_mse_incl is_module senv.env mp_sup inl me in - let senv = add_constraints (Now (false, cst)) senv in + let senv = add_constraints (Now cst) senv in (* Include Self support *) let rec compute_sign sign mb resolver senv = match sign with @@ -1036,7 +1046,7 @@ let add_include me is_module inl senv = let cst_sub = Subtyping.check_subtypes senv.env mb mtb in let senv = add_constraints - (Now (false, Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) + (Now (Univ.ContextSet.add_constraints cst_sub Univ.ContextSet.empty)) senv in let mpsup_delta = Modops.inline_delta_resolver senv.env inl mp_sup mbid mtb mb.mod_delta @@ -1266,7 +1276,7 @@ let register_inductive ind prim senv = let add_constraints c = add_constraints - (Now (false, Univ.ContextSet.add_constraints c Univ.ContextSet.empty)) + (Now (Univ.ContextSet.add_constraints c Univ.ContextSet.empty)) (* NB: The next old comment probably refers to [propagate_loads] above. diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 3e902303c3..885becc40a 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.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/kernel/sorts.ml b/kernel/sorts.ml index b5a929697e..b8bebb659b 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.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/kernel/sorts.mli b/kernel/sorts.mli index 3769e31465..fa129d10fb 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.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/kernel/subtyping.ml b/kernel/subtyping.ml index 24845ce459..d47dc0c6e1 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.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/kernel/subtyping.mli b/kernel/subtyping.mli index 4e755e42ff..9aa48bf6b4 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.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/kernel/term.ml b/kernel/term.ml index f09c45715f..38c0d043cf 100644 --- a/kernel/term.ml +++ b/kernel/term.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/kernel/term.mli b/kernel/term.mli index 4265324693..d2de4177ce 100644 --- a/kernel/term.mli +++ b/kernel/term.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/kernel/term_typing.ml b/kernel/term_typing.ml index f984088f47..165feca1b6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.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 *) @@ -79,7 +79,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = Undef nl; cook_type = t; cook_universes = univs; - cook_private_univs = None; cook_relevance = r; cook_inline = false; cook_context = ctx; @@ -108,7 +107,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = { Cooking.cook_body = cd; cook_type = ty; cook_universes = Monomorphic uctxt; - cook_private_univs = None; cook_inline = false; cook_context = None; cook_relevance = Sorts.Relevant; @@ -124,7 +122,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in let tyj = Typeops.infer_type env typ in let proofterm = - Future.chain body (fun ((body,uctx),side_eff) -> + Future.chain body begin fun ((body,uctx),side_eff) -> (* don't redeclare universes which are declared for the type *) let uctx = Univ.ContextSet.diff uctx univs in let j, uctx = match trust with @@ -145,13 +143,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = in let c = j.uj_val in feedback_completion_typecheck feedback_id; - c, uctx) in + c, Opaqueproof.PrivateMonomorphic uctx + end in let def = OpaqueDef proofterm in { Cooking.cook_body = def; cook_type = tyj.utj_val; cook_universes = Monomorphic univs; - cook_private_univs = None; cook_relevance = Sorts.relevance_of_sort tyj.utj_type; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -168,8 +166,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let tj = Typeops.infer_type env typ in let sbst, auctx = Univ.abstract_universes nas uctx in let usubst = Univ.make_instance_subst sbst in - let (def, private_univs) = - let (body, ctx), side_eff = Future.join body in + let proofterm = Future.chain body begin fun ((body, ctx), side_eff) -> let body, ctx = match trust with | Pure -> body, ctx | SideEffects handle -> @@ -183,16 +180,15 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = let j = Typeops.infer env body in let _ = Typeops.judge_of_cast env j DEFAULTcast tj in let def = Vars.subst_univs_level_constr usubst j.uj_val in - def, private_univs - in - let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in + let () = feedback_completion_typecheck feedback_id in + def, Opaqueproof.PrivatePolymorphic (Univ.AUContext.size auctx, private_univs) + end in + let def = OpaqueDef proofterm in let typ = Vars.subst_univs_level_constr usubst tj.utj_val in - feedback_completion_typecheck feedback_id; { Cooking.cook_body = def; cook_type = typ; cook_universes = Polymorphic auctx; - cook_private_univs = Some private_univs; cook_relevance = Sorts.relevance_of_sort tj.utj_type; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -211,22 +207,22 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = body, ctx | SideEffects _ -> assert false in - let env, usubst, univs, private_univs = match c.const_entry_universes with + let env, usubst, univs = match c.const_entry_universes with | Monomorphic_entry univs -> let ctx = Univ.ContextSet.union univs ctx in let env = push_context_set ~strict:true ctx env in - env, Univ.empty_level_subst, Monomorphic ctx, None + env, Univ.empty_level_subst, Monomorphic ctx | Polymorphic_entry (nas, uctx) -> (** [ctx] must contain local universes, such that it has no impact on the rest of the graph (up to transitivity). *) let env = push_context ~strict:false uctx env in let sbst, auctx = Univ.abstract_universes nas uctx in let sbst = Univ.make_instance_subst sbst in - let env, local = - if Univ.ContextSet.is_empty ctx then env, None - else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") + let () = + if not (Univ.ContextSet.is_empty ctx) then + CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.") in - env, sbst, Polymorphic auctx, local + env, sbst, Polymorphic auctx in let j = Typeops.infer env body in let typ = match typ with @@ -244,7 +240,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; - cook_private_univs = private_univs; cook_relevance = Retypeops.relevance_of_term env j.uj_val; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; @@ -341,7 +336,6 @@ let build_constant_declaration env result = const_type = typ; const_body_code = tps; const_universes = univs; - const_private_poly_univs = result.cook_private_univs; const_relevance = result.cook_relevance; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } @@ -368,7 +362,6 @@ let translate_recipe env _kn r = const_type = result.cook_type; const_body_code = tps; const_universes = univs; - const_private_poly_univs = result.cook_private_univs; const_relevance = result.cook_relevance; const_inline_code = result.cook_inline; const_typing_flags = Environ.typing_flags env } @@ -407,7 +400,10 @@ let translate_local_def env _id centry = let (p, cst) = Future.force o in (** Let definitions are ensured to have no extra constraints coming from the body by virtue of the typing of [Entries.section_def_entry]. *) - let () = assert (Univ.ContextSet.is_empty cst) in + let () = match cst with + | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx) + | Opaqueproof.PrivatePolymorphic (_, ctx) -> assert (Univ.ContextSet.is_empty ctx) + in p | Undef _ | Primitive _ -> assert false in diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index fd0f2a18e4..225abd60f8 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.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/kernel/transparentState.ml b/kernel/transparentState.ml index 9661dace6a..372e021c39 100644 --- a/kernel/transparentState.ml +++ b/kernel/transparentState.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/kernel/transparentState.mli b/kernel/transparentState.mli index f2999c6869..db6d147280 100644 --- a/kernel/transparentState.mli +++ b/kernel/transparentState.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/kernel/type_errors.ml b/kernel/type_errors.ml index 857e4fabf7..f221ac7a4f 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.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/kernel/type_errors.mli b/kernel/type_errors.mli index 8e25236851..ae6fd31762 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.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/kernel/typeops.ml b/kernel/typeops.ml index af710e7822..b87384d228 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.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/kernel/typeops.mli b/kernel/typeops.mli index c8f3e506e6..c71a0e0ca4 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.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/kernel/uGraph.ml b/kernel/uGraph.ml index 0d5b55ca1b..6fde6e9c5f 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.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/kernel/uGraph.mli b/kernel/uGraph.mli index 17d6c6e6d3..e1b5868d55 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.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/kernel/uint63_amd64_63.ml b/kernel/uint63_amd64_63.ml index 2d4d685775..20b2f58496 100644 --- a/kernel/uint63_amd64_63.ml +++ b/kernel/uint63_amd64_63.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/kernel/uint63_i386_31.ml b/kernel/uint63_i386_31.ml index fa45c90241..c3279779e1 100644 --- a/kernel/uint63_i386_31.ml +++ b/kernel/uint63_i386_31.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/kernel/univ.ml b/kernel/univ.ml index 2b88d6884d..14d6bfabf1 100644 --- a/kernel/univ.ml +++ b/kernel/univ.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/kernel/univ.mli b/kernel/univ.mli index ddb204dd52..ccb5c80cbf 100644 --- a/kernel/univ.mli +++ b/kernel/univ.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/kernel/vars.ml b/kernel/vars.ml index bd56d60053..dd187387d4 100644 --- a/kernel/vars.ml +++ b/kernel/vars.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/kernel/vars.mli b/kernel/vars.mli index f2c32b3625..6a1815619f 100644 --- a/kernel/vars.mli +++ b/kernel/vars.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/kernel/vconv.mli b/kernel/vconv.mli index 1a31848989..0a85498c40 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.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/kernel/vm.ml b/kernel/vm.ml index 83312a8530..319a26d824 100644 --- a/kernel/vm.ml +++ b/kernel/vm.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/kernel/vm.mli b/kernel/vm.mli index 50ebc90626..5637f7e1cd 100644 --- a/kernel/vm.mli +++ b/kernel/vm.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/kernel/vmvalues.ml b/kernel/vmvalues.ml index 88fcb71e77..c8f5020d71 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.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/kernel/vmvalues.mli b/kernel/vmvalues.mli index 6d984d5f49..d289e7db9a 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.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/kernel/write_uint63.ml b/kernel/write_uint63.ml index 42bb5dfbb1..57a170c8f5 100644 --- a/kernel/write_uint63.ml +++ b/kernel/write_uint63.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 *) |