diff options
Diffstat (limited to 'kernel')
108 files changed, 496 insertions, 411 deletions
diff --git a/kernel/byterun/coq_float64.h b/kernel/byterun/coq_float64.h index c41079c8ff..84a3edf1c7 100644 --- a/kernel/byterun/coq_float64.h +++ b/kernel/byterun/coq_float64.h @@ -1,3 +1,13 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ +/* \VV/ **************************************************************/ +/* // * This file is distributed under the terms of the */ +/* * GNU Lesser General Public License Version 2.1 */ +/* * (see LICENSE file for the text of the license) */ +/************************************************************************/ + #ifndef _COQ_FLOAT64_ #define _COQ_FLOAT64_ diff --git a/kernel/byterun/coq_gc.h b/kernel/byterun/coq_gc.h deleted file mode 100644 index 38eda4d11f..0000000000 --- a/kernel/byterun/coq_gc.h +++ /dev/null @@ -1,59 +0,0 @@ -/***********************************************************************/ -/* */ -/* Coq Compiler */ -/* */ -/* Benjamin Gregoire, projets Logical and Cristal */ -/* INRIA Rocquencourt */ -/* */ -/* */ -/***********************************************************************/ - -#ifndef _COQ_CAML_GC_ -#define _COQ_CAML_GC_ -#include <caml/mlvalues.h> -#include <caml/alloc.h> -#include <caml/memory.h> - -typedef void (*scanning_action) (value, value *); - - -CAMLextern char *young_ptr; -CAMLextern char *young_limit; -CAMLextern void (*scan_roots_hook) (scanning_action); -CAMLextern void minor_collection (void); - -#define Caml_white (0 << 8) -#define Caml_black (3 << 8) - -#ifdef HAS_OCP_MEMPROF - -/* This code is necessary to make the OCamlPro memory profiling branch of - OCaml compile. */ - -#define Make_header(wosize, tag, color) \ - caml_make_header(wosize, tag, color) - -#else - -#define Make_header(wosize, tag, color) \ - (((header_t) (((header_t) (wosize) << 10) \ - + (color) \ - + (tag_t) (tag))) \ - ) -#endif - -#define Alloc_small(result, wosize, tag) do{ \ - young_ptr -= Bhsize_wosize (wosize); \ - if (young_ptr < young_limit){ \ - young_ptr += Bhsize_wosize (wosize); \ - Setup_for_gc; \ - minor_collection (); \ - Restore_after_gc; \ - young_ptr -= Bhsize_wosize (wosize); \ - } \ - Hd_hp (young_ptr) = Make_header ((wosize), (tag), Caml_black); \ - (result) = Val_hp (young_ptr); \ - }while(0) - - -#endif /*_COQ_CAML_GC_ */ diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index 606cce0127..7588c1ce07 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -16,17 +16,37 @@ #include <stdio.h> #include <signal.h> #include <stdint.h> +#include <math.h> + +#define CAML_INTERNALS #include <caml/memory.h> #include <caml/signals.h> #include <caml/version.h> -#include <math.h> -#include "coq_gc.h" + #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" #include "coq_values.h" #include "coq_float64.h" +#if OCAML_VERSION < 41000 +extern void caml_minor_collection(void); + +#undef Alloc_small +#define Alloc_small(result, wosize, tag) do{ \ + caml_young_ptr -= Bhsize_wosize(wosize); \ + if (caml_young_ptr < caml_young_limit) { \ + caml_young_ptr += Bhsize_wosize(wosize); \ + Setup_for_gc; \ + caml_minor_collection(); \ + Restore_after_gc; \ + caml_young_ptr -= Bhsize_wosize(wosize); \ + } \ + Hd_hp(caml_young_ptr) = Make_header((wosize), (tag), Caml_black); \ + (result) = Val_hp(caml_young_ptr); \ + }while(0) +#endif + #ifdef ARCH_SIXTYFOUR #include "coq_uint63_native.h" #else diff --git a/kernel/byterun/coq_memory.c b/kernel/byterun/coq_memory.c index 91d6773b1f..6233675c66 100644 --- a/kernel/byterun/coq_memory.c +++ b/kernel/byterun/coq_memory.c @@ -10,9 +10,12 @@ #include <stdio.h> #include <string.h> + +#define CAML_INTERNALS #include <caml/alloc.h> #include <caml/address_class.h> -#include "coq_gc.h" +#include <caml/roots.h> + #include "coq_instruct.h" #include "coq_fix_code.h" #include "coq_memory.h" diff --git a/kernel/byterun/coq_uint63_emul.h b/kernel/byterun/coq_uint63_emul.h index 143a6d098c..d92bbe87eb 100644 --- a/kernel/byterun/coq_uint63_emul.h +++ b/kernel/byterun/coq_uint63_emul.h @@ -1,3 +1,13 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ +/* \VV/ **************************************************************/ +/* // * This file is distributed under the terms of the */ +/* * GNU Lesser General Public License Version 2.1 */ +/* * (see LICENSE file for the text of the license) */ +/************************************************************************/ + # pragma once # include <caml/callback.h> diff --git a/kernel/byterun/coq_uint63_native.h b/kernel/byterun/coq_uint63_native.h index 5be7587091..27696e8856 100644 --- a/kernel/byterun/coq_uint63_native.h +++ b/kernel/byterun/coq_uint63_native.h @@ -1,3 +1,13 @@ +/************************************************************************/ +/* * The Coq Proof Assistant / The Coq Development Team */ +/* v * Copyright INRIA, CNRS and contributors */ +/* <O___,, * (see version control and CREDITS file for authors & dates) */ +/* \VV/ **************************************************************/ +/* // * This file is distributed under the terms of the */ +/* * GNU Lesser General Public License Version 2.1 */ +/* * (see LICENSE file for the text of the license) */ +/************************************************************************/ + #define Is_uint63(v) (Is_long(v)) #define uint_of_value(val) (((uint64_t)(val)) >> 1) diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index af08ea18c1..1316dfe069 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index 720f11b8f2..9e94248113 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 9ff7f69203..3fa376a037 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index be65ba5305..2a0399f1f7 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index e33a4f1518..25ec250367 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index d7ea6f13c2..f1d441ca76 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 985c692eea..050f986367 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 38c1c45a85..d5ea2509ef 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 4e22421f56..d855dbf2bb 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 9184164504..209d741ba8 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/constr.ml b/kernel/constr.ml index 84eacb196c..ade03fdf93 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -1297,7 +1297,8 @@ let hashcons (sh_sort,sh_ci,sh_construct,sh_ind,sh_con,sh_na,sh_id) = fun t -> fst (sh_rec t) (* Exported hashing fonction on constr, used mainly in plugins. - Appears to have slight differences from [snd (hash_term t)] above ? *) + Slight differences from [snd (hash_term t)] above: it ignores binders + and doesn't do [land 0x3FFFFFFF]. *) let rec hash t = match kind t with @@ -1336,7 +1337,7 @@ let rec hash t = | Float f -> combinesmall 19 (Float64.hash f) and hash_term_array t = - Array.fold_left (fun acc t -> combine (hash t) acc) 0 t + Array.fold_left (fun acc t -> combine acc (hash t)) 0 t module CaseinfoHash = struct diff --git a/kernel/constr.mli b/kernel/constr.mli index 159570b5ea..16919b705a 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/context.ml b/kernel/context.ml index 500ed20343..6a99f201f3 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/context.mli b/kernel/context.mli index 04aa039a01..76c4461760 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 7ce320381c..9b87c194c5 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 4887e70cdb..b25488d94a 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 31dd26d2ba..a17aff9b09 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -295,20 +295,14 @@ let abstract_projection ~params expmod hyps t = t let cook_one_ind ~ntypes - (section_decls,_ as hyps) expmod mip = + hyps expmod mip = let mind_arity = match mip.mind_arity with | RegularArity {mind_user_arity=arity;mind_sort=sort} -> let arity = abstract_as_type (expmod arity) hyps in let sort = destSort (expmod (mkSort sort)) in RegularArity {mind_user_arity=arity; mind_sort=sort} - | TemplateArity {template_param_levels=levels;template_level;template_context} -> - let sec_levels = CList.map_filter (fun d -> - if RelDecl.is_local_assum d then Some None - else None) - section_decls - in - let levels = List.rev_append sec_levels levels in - TemplateArity {template_param_levels=levels;template_level;template_context} + | TemplateArity {template_level} -> + TemplateArity {template_level} in let mind_arity_ctxt = let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in @@ -386,6 +380,17 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = in Some (Array.append newvariance variance), Some sec_variance in + let mind_template = match mib.mind_template with + | None -> None + | Some {template_param_levels=levels; template_context} -> + let sec_levels = CList.map_filter (fun d -> + if RelDecl.is_local_assum d then Some None + else None) + section_decls + in + let levels = List.rev_append sec_levels levels in + Some {template_param_levels=levels; template_context} + in { mind_packets; mind_record; @@ -396,6 +401,7 @@ let cook_inductive { Opaqueproof.modlist; abstract } mib = mind_nparams_rec = mib.mind_nparams_rec + nnewparams; mind_params_ctxt; mind_universes; + mind_template; mind_variance; mind_sec_variance; mind_private = mib.mind_private; diff --git a/kernel/cooking.mli b/kernel/cooking.mli index c2d47735ec..8d45b259be 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 978c2c9f57..f41585e93a 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index 3322c89aa9..e480bfcec1 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index ac130d018d..244cd2865d 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -30,8 +30,11 @@ type engagement = set_predicativity *) type template_arity = { - template_param_levels : Univ.Level.t option list; template_level : Univ.Universe.t; +} + +type template_universes = { + template_param_levels : Univ.Level.t option list; template_context : Univ.ContextSet.t; } @@ -218,6 +221,8 @@ type mutual_inductive_body = { mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *) + mind_template : template_universes option; + mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *) mind_sec_variance : Univ.Variance.t array option; diff --git a/kernel/declareops.ml b/kernel/declareops.ml index a3adac7a11..20dc21900c 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -46,9 +46,10 @@ let map_decl_arity f g = function | TemplateArity a -> TemplateArity (g a) let hcons_template_arity ar = + { template_level = Univ.hcons_univ ar.template_level; } + +let hcons_template_universe ar = { template_param_levels = ar.template_param_levels; - (* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *) - template_level = Univ.hcons_univ ar.template_level; template_context = Univ.hcons_universe_context_set ar.template_context } let universes_context = function @@ -247,6 +248,7 @@ let subst_mind_body sub mib = Context.Rel.map (subst_mps sub) mib.mind_params_ctxt; mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ; mind_universes = mib.mind_universes; + mind_template = mib.mind_template; mind_variance = mib.mind_variance; mind_sec_variance = mib.mind_sec_variance; mind_private = mib.mind_private; @@ -323,6 +325,7 @@ let hcons_mind mib = { mib with mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets; mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt; + mind_template = Option.Smart.map hcons_template_universe mib.mind_template; mind_universes = hcons_universes mib.mind_universes } (** Hashconsing of modules *) diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 5a1331afa9..01e4429e7e 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/entries.ml b/kernel/entries.ml index 8d930b521c..e0b678621a 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -37,7 +37,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1]; type one_inductive_entry = { mind_entry_typename : Id.t; mind_entry_arity : constr; - mind_entry_template : bool; (* Use template polymorphism *) mind_entry_consnames : Id.t list; mind_entry_lc : constr list } @@ -50,6 +49,7 @@ type mutual_inductive_entry = { mind_entry_params : Constr.rel_context; mind_entry_inds : one_inductive_entry list; mind_entry_universes : universes_entry; + mind_entry_template : bool; (* Use template polymorphism *) mind_entry_cumulative : bool; (* universe constraints and the constraints for subtyping of inductive types in the block. *) diff --git a/kernel/environ.ml b/kernel/environ.ml index 501ac99ff3..2d2c9a454b 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -590,11 +590,11 @@ let template_polymorphic_ind (mind,i) env = | TemplateArity _ -> true | RegularArity _ -> false -let template_polymorphic_variables (mind,i) env = - match (lookup_mind mind env).mind_packets.(i).mind_arity with - | TemplateArity { Declarations.template_param_levels = l; _ } -> +let template_polymorphic_variables (mind, _) env = + match (lookup_mind mind env).mind_template with + | Some { Declarations.template_param_levels = l; _ } -> List.map_filter (fun level -> level) l - | RegularArity _ -> [] + | None -> [] let template_polymorphic_pind (ind,u) env = if not (Univ.Instance.is_empty u) then false diff --git a/kernel/environ.mli b/kernel/environ.mli index a596584cbe..25ecdfd852 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/esubst.ml b/kernel/esubst.ml index f10cf20b42..3e8502b988 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index a1a5b5251a..4239e42adc 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/evar.ml b/kernel/evar.ml index a0bed31f68..48b050e591 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/evar.mli b/kernel/evar.mli index 25a92d3e1d..8dce622477 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/float64.ml b/kernel/float64.ml index cc661aeba3..299f53e8ab 100644 --- a/kernel/float64.ml +++ b/kernel/float64.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/float64.mli b/kernel/float64.mli index 2aa9796526..d43ff4553f 100644 --- a/kernel/float64.mli +++ b/kernel/float64.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) -(* <O___,, * (see CREDITS file for the list of authors) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/genOpcodeFiles.ml b/kernel/genOpcodeFiles.ml index 82bb2b584d..0a9f137c45 100644 --- a/kernel/genOpcodeFiles.ml +++ b/kernel/genOpcodeFiles.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml index cc15109f06..8ac96a6481 100644 --- a/kernel/indTyping.ml +++ b/kernel/indTyping.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -101,10 +101,10 @@ let check_indices_matter env_params info indices = else check_context_univs ~ctor:false env_params info indices (* env_ar contains the inductives before the current ones in the block, and no parameters *) -let check_arity env_params env_ar ind = +let check_arity ~template env_params env_ar ind = let {utj_val=arity;utj_type=_} = Typeops.infer_type env_params ind.mind_entry_arity in let indices, ind_sort = Reduction.dest_arity env_params arity in - let ind_min_univ = if ind.mind_entry_template then Some Universe.type0m else None in + let ind_min_univ = if template then Some Universe.type0m else None in let univ_info = { ind_squashed=false; ind_has_relevant_arg=false; @@ -200,28 +200,88 @@ let unbounded_from_below u cstrs = let template_polymorphic_univs ~ctor_levels uctx paramsctxt concl = let check_level l = Univ.LSet.mem l (Univ.ContextSet.levels uctx) && + (let () = assert (not @@ Univ.Level.is_small l) in true) && unbounded_from_below l (Univ.ContextSet.constraints uctx) && not (Univ.LSet.mem l ctor_levels) in let univs = Univ.Universe.levels concl in - let univs = - Univ.LSet.filter (fun l -> check_level l || Univ.Level.is_prop l) univs - in + let univs = Univ.LSet.filter (fun l -> check_level l) univs in let fold acc = function | (LocalAssum (_, p)) -> (let c = Term.strip_prod_assum p in match kind c with | Sort (Type u) -> (match Univ.Universe.level u with - | Some l -> if Univ.LSet.mem l univs && not (Univ.Level.is_prop l) then Some l else None + | Some l -> if Univ.LSet.mem l univs then Some l else None | None -> None) | _ -> None) :: acc | LocalDef _ -> acc in let params = List.fold_left fold [] paramsctxt in - params, univs + if Universe.is_type0m concl then Some (univs, params) + else if not @@ Univ.LSet.is_empty univs then Some (univs, params) + else None + +let get_param_levels ctx params arity splayed_lc = + let min_univ = match arity with + | RegularArity _ -> + CErrors.user_err + Pp.(strbrk "Ill-formed template mutual inductive declaration: all types must be template.") + | TemplateArity ar -> ar.template_level + in + let ctor_levels = + let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in + let param_levels = + List.fold_left (fun levels d -> match d with + | LocalAssum _ -> levels + | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) + Univ.LSet.empty params + in + Array.fold_left + (fun levels (d,c) -> + let levels = + List.fold_left (fun levels d -> + Context.Rel.Declaration.fold_constr add_levels d levels) + levels d + in + add_levels c levels) + param_levels + splayed_lc + in + match template_polymorphic_univs ~ctor_levels ctx params min_univ with + | None -> + CErrors.user_err + Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") + | Some (_, param_levels) -> + param_levels + +let get_template univs params data = + let ctx = match univs with + | Monomorphic ctx -> ctx + | Polymorphic _ -> + CErrors.anomaly ~label:"polymorphic_template_ind" + Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in + (* For each type in the block, compute potential template parameters *) + let params = List.map (fun ((arity, _), (_, splayed_lc), _) -> get_param_levels ctx params arity splayed_lc) data in + (* Pick the lower bound of template parameters. Note that in particular, if + one of the the inductive types from the block is Prop-valued, then no + parameters are template. *) + let fold min params = + let map u v = match u, v with + | (None, _) | (_, None) -> None + | Some u, Some v -> + let () = assert (Univ.Level.equal u v) in + Some u + in + List.map2 map min params + in + let params = match params with + | [] -> assert false + | hd :: rem -> List.fold_left fold hd rem + in + { template_param_levels = params; template_context = ctx } -let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) = +let abstract_packets usubst ((arity,lc),(indices,splayed_lc),univ_info) = if not (Universe.Set.is_empty univ_info.missing) then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ))); let arity = Vars.subst_univs_level_constr usubst arity in @@ -237,40 +297,7 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i let arity = match univ_info.ind_min_univ with | None -> RegularArity {mind_user_arity = arity; mind_sort = Sorts.sort_of_univ ind_univ} - | Some min_univ -> - let ctx = match univs with - | Monomorphic ctx -> ctx - | Polymorphic _ -> - CErrors.anomaly ~label:"polymorphic_template_ind" - Pp.(strbrk "Template polymorphism and full polymorphism are incompatible.") in - let ctor_levels = - let add_levels c levels = Univ.LSet.union levels (Vars.universes_of_constr c) in - let param_levels = - List.fold_left (fun levels d -> match d with - | LocalAssum _ -> levels - | LocalDef (_,b,t) -> add_levels b (add_levels t levels)) - Univ.LSet.empty params - in - Array.fold_left - (fun levels (d,c) -> - let levels = - List.fold_left (fun levels d -> - Context.Rel.Declaration.fold_constr add_levels d levels) - levels d - in - add_levels c levels) - param_levels - splayed_lc - in - let param_levels, concl_levels = - template_polymorphic_univs ~ctor_levels ctx params min_univ - in - if List.for_all (fun x -> Option.is_empty x) param_levels - && Univ.LSet.is_empty concl_levels then - CErrors.user_err - Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.") - else - TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx } + | Some min_univ -> TemplateArity { template_level = min_univ; } in let kelim = allowed_sorts univ_info in @@ -285,7 +312,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = mind_check_names mie; assert (List.is_empty (Environ.rel_context env)); - let has_template_poly = List.exists (fun oie -> oie.mind_entry_template) mie.mind_entry_inds in + let has_template_poly = mie.mind_entry_template in (* universes *) let env_univs = @@ -306,7 +333,7 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = let env_params, params = Typeops.check_context env_univs mie.mind_entry_params in (* Arities *) - let env_ar, data = List.fold_left_map (check_arity env_params) env_univs mie.mind_entry_inds in + let env_ar, data = List.fold_left_map (check_arity ~template:has_template_poly env_params) env_univs mie.mind_entry_inds in let env_ar_par = push_rel_context params env_ar in (* Constructors *) @@ -352,7 +379,14 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = (* Abstract universes *) let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in let params = Vars.subst_univs_level_context usubst params in - let data = List.map (abstract_packets univs usubst params) data in + let data = List.map (abstract_packets usubst) data in + let template = + let check ((arity, _), _, _) = match arity with + | TemplateArity _ -> true + | RegularArity _ -> false + in + if List.exists check data then Some (get_template univs params data) else None + in let env_ar_par = let ctx = Environ.rel_context env_ar_par in @@ -361,4 +395,4 @@ let typecheck_inductive env ~sec_univs (mie:mutual_inductive_entry) = Environ.push_rel_context ctx env in - env_ar_par, univs, variance, record, params, Array.of_list data + env_ar_par, univs, template, variance, record, params, Array.of_list data diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli index 723ba5459e..5c239ce8a8 100644 --- a/kernel/indTyping.mli +++ b/kernel/indTyping.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -29,6 +29,7 @@ val typecheck_inductive : env -> sec_univs:Univ.Level.t array option -> mutual_inductive_entry -> env * universes + * template_universes option * Univ.Variance.t array option * Names.Id.t array option option * Constr.rel_context @@ -44,4 +45,4 @@ val template_polymorphic_univs : Univ.ContextSet.t -> Constr.rel_context -> Univ.Universe.t -> - Univ.Level.t option list * Univ.LSet.t + (Univ.LSet.t * Univ.Level.t option list) option diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b6b8e5265c..9da6c7842e 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -102,7 +102,7 @@ let failwith_non_pos_list n ntypes l = (* Check the inductive type is called with the expected parameters *) (* [n] is the index of the last inductive type in [env] *) -let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = +let check_correct_par ~chkpos (env,n,ntypes,_) paramdecls ind_index args = let nparams = Context.Rel.nhyps paramdecls in let args = Array.of_list args in if Array.length args < nparams then @@ -123,7 +123,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = LocalNonPar (param_index+1, paramdecl_index_in_env, ind_index) in raise (IllFormedInd err) in check (nparams-1) (n-nparamdecls) paramdecls; - if not (Array.for_all (noccur_between n ntypes) realargs) then + if chkpos && not (Array.for_all (noccur_between n ntypes) realargs) then failwith_non_pos_vect n ntypes realargs (* Computes the maximum number of recursive parameters: @@ -325,7 +325,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( if check_head then begin match hd with | Rel j when Int.equal j (n + ntypes - i - 1) -> - check_correct_par ienv paramsctxt (ntypes - i) largs + check_correct_par ~chkpos ienv paramsctxt (ntypes - i) largs | _ -> raise (IllFormedInd (LocalNotConstructor(paramsctxt,nnonrecargs))) end else @@ -466,7 +466,7 @@ let compute_projections (kn, i as ind) mib = Array.of_list (List.rev rs), Array.of_list (List.rev pbs) -let build_inductive env ~sec_univs names prv univs variance +let build_inductive env ~sec_univs names prv univs template variance paramsctxt kn isrecord isfinite inds nmr recargs = let ntypes = Array.length inds in (* Compute the set of used section variables *) @@ -538,6 +538,7 @@ let build_inductive env ~sec_univs names prv univs variance mind_params_ctxt = paramsctxt; mind_packets = packets; mind_universes = univs; + mind_template = template; mind_variance = variance; mind_sec_variance = sec_variance; mind_private = prv; @@ -562,7 +563,7 @@ let build_inductive env ~sec_univs names prv univs variance let check_inductive env ~sec_univs kn mie = (* First type-check the inductive definition *) - let (env_ar_par, univs, variance, record, paramsctxt, inds) = + let (env_ar_par, univs, template, variance, record, paramsctxt, inds) = IndTyping.typecheck_inductive env ~sec_univs mie in (* Then check positivity conditions *) @@ -575,6 +576,6 @@ let check_inductive env ~sec_univs kn mie = (Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds) in (* Build the inductive packets *) - build_inductive env ~sec_univs names mie.mind_entry_private univs variance + build_inductive env ~sec_univs names mie.mind_entry_private univs template variance paramsctxt kn record mie.mind_entry_finite inds nmr recargs diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 9b54e8b878..f194ab2883 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 1be86f2bf8..8423813639 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -185,8 +185,8 @@ let make_subst = exception SingletonInductiveBecomesProp of Id.t -let instantiate_universes ctx ar args = - let subst = make_subst (ctx,ar.template_param_levels,args) in +let instantiate_universes ctx (templ, ar) args = + let subst = make_subst (ctx,templ.template_param_levels,args) in let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) @@ -215,8 +215,12 @@ let type_of_inductive_gen ?(polyprop=true) ((mib,mip),u) paramtyps = match mip.mind_arity with | RegularArity a -> subst_instance_constr u a.mind_user_arity | TemplateArity ar -> + let templ = match mib.mind_template with + | None -> assert false + | Some t -> t + in let ctx = List.rev mip.mind_arity_ctxt in - let ctx,s = instantiate_universes ctx ar paramtyps in + let ctx,s = instantiate_universes ctx (templ, ar) paramtyps in (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. the situation where a non-Prop singleton inductive becomes Prop when applied to Prop params *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index b690fe1157..9f865f8f01 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -123,9 +123,6 @@ exception SingletonInductiveBecomesProp of Id.t val max_inductive_sort : Sorts.t array -> Universe.t -val instantiate_universes : Constr.rel_context -> - template_arity -> param_univs -> Constr.rel_context * Sorts.t - (** {6 Debug} *) type size = Large | Strict diff --git a/kernel/inferCumulativity.ml b/kernel/inferCumulativity.ml index 211c909241..f987164d52 100644 --- a/kernel/inferCumulativity.ml +++ b/kernel/inferCumulativity.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/inferCumulativity.mli b/kernel/inferCumulativity.mli index a8f593c7f9..db5539a0ff 100644 --- a/kernel/inferCumulativity.mli +++ b/kernel/inferCumulativity.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index f1e994b337..cc9da3a2ce 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -27,7 +27,7 @@ Conv_oracle Environ Primred CClosure -Retypeops +Relevanceops Reduction Clambda Nativelambda diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 1cf34977c5..aa513c1536 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index b69e62b8a6..bc5816dafb 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index c1ac8b1a3e..76e2a584bd 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index aa8aa96746..fd5421aefe 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/modops.ml b/kernel/modops.ml index 2b141cc6a7..301af328e4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -382,21 +382,21 @@ let inline_delta_resolver env inl mp mbid mtb delta = let rec make_inline delta = function | [] -> delta | (lev,kn)::r -> - let kn = replace_mp_in_kn (MPbound mbid) mp kn in - let con = constant_of_delta_kn delta kn in - try - let constant = lookup_constant con env in - let l = make_inline delta r in - match constant.const_body with - | Undef _ | OpaqueDef _ | Primitive _ -> l - | Def body -> - let constr = Mod_subst.force_constr body in - let ctx = Declareops.constant_polymorphic_context constant in - let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in - add_inline_delta_resolver kn (lev, Some constr) l - with Not_found -> - error_no_such_label_sub (Constant.label con) - (ModPath.to_string (Constant.modpath con)) + let kn = replace_mp_in_kn (MPbound mbid) mp kn in + let con = constant_of_delta_kn delta kn in + if not (Environ.mem_constant con env) then + error_no_such_label_sub (Constant.label con) + (ModPath.to_string (Constant.modpath con)) + else + let constant = lookup_constant con env in + let l = make_inline delta r in + match constant.const_body with + | Undef _ | OpaqueDef _ | Primitive _ -> l + | Def body -> + let constr = Mod_subst.force_constr body in + let ctx = Declareops.constant_polymorphic_context constant in + let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in + add_inline_delta_resolver kn (lev, Some constr) l in make_inline delta constants diff --git a/kernel/modops.mli b/kernel/modops.mli index badbd973ae..ed8598d51b 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/names.ml b/kernel/names.ml index 148cc352f1..592b5e65f7 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/names.mli b/kernel/names.mli index d43038d2f0..ea137ad1f4 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index ec3f15176b..f30ddce4d7 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index ed395368b2..71317d188b 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index c3710cb0d6..31a716a786 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 9cacf0f4ef..900ed5e480 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index ad71557a65..9ed0f6f411 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 1d7bf5343a..e339286329 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 3f2e63b984..dde1274152 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index 155fde54e9..29b4d20197 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index 7f46d4e173..c95880dc36 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index c53a626528..8f58dfa8d3 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 891b4bf8f7..6cfe44c5ff 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 420249117d..78a9b2ea13 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index 774bdc92fb..e5342754c4 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index 1870241dcd..016fcf4fef 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/reduction.ml b/kernel/reduction.ml index b7bd4eef9a..469d5ccaa2 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -331,7 +331,7 @@ let skip_pattern infos n c1 c2 = let is_irrelevant infos lft c = let env = info_env infos.cnv_inf in - try Retypeops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false + try Relevanceops.relevance_of_fterm env infos.relevances lft c == Sorts.Irrelevant with _ -> false (* Conversion between [lft1]term1 and [lft2]term2 *) let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv = diff --git a/kernel/reduction.mli b/kernel/reduction.mli index ecd6b89388..ff5934c66c 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/retypeops.ml b/kernel/relevanceops.ml index 6a1b36ea94..3f3e722245 100644 --- a/kernel/retypeops.ml +++ b/kernel/relevanceops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/retypeops.mli b/kernel/relevanceops.mli index dd4513959f..86734e747e 100644 --- a/kernel/retypeops.mli +++ b/kernel/relevanceops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 479fe02295..4e642ca11d 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 2df8a00465..bf8ec8badb 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d8e1b6537e..181ec4860c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -249,11 +249,52 @@ let check_engagement env expected_impredicative_set = (** {6 Stm machinery } *) +module Certificate : +sig + type t + + val make : safe_environment -> t + + val universes : t -> Univ.ContextSet.t + + (** Checks whether [dst] is a valid extension of [src] *) + val check : src:t -> dst:t -> bool +end = +struct + +type t = { + certif_struc : Declarations.structure_body; + certif_univs : Univ.ContextSet.t; +} + +let make senv = { + certif_struc = senv.revstruct; + certif_univs = senv.univ; +} + +let is_suffix l suf = match l with +| [] -> false +| _ :: l -> l == suf + +let is_subset (s1, cst1) (s2, cst2) = + Univ.LSet.subset s1 s2 && Univ.Constraint.subset cst1 cst2 + +let check ~src ~dst = + is_suffix dst.certif_struc src.certif_struc && + is_subset src.certif_univs dst.certif_univs + +let universes c = c.certif_univs + +end + type side_effect = { - from_env : Declarations.structure_body CEphemeron.key; + seff_certif : Certificate.t CEphemeron.key; seff_constant : Constant.t; seff_body : Constr.t Declarations.constant_body; } +(* Invariant: For any senv, if [Certificate.check senv seff_certif] then + senv where univs := Certificate.universes seff_certif] + + (c.seff_constant -> seff_body) is well-formed. *) module SideEffects : sig @@ -609,7 +650,7 @@ let inline_side_effects env body side_eff = let filter e = let cb = (e.seff_constant, e.seff_body) in if Environ.mem_constant e.seff_constant env then None - else Some (cb, e.from_env) + else Some (cb, e.seff_certif) in (* CAVEAT: we assure that most recent effects come first *) let side_eff = List.map_filter filter (SideEffects.repr side_eff) in @@ -678,28 +719,27 @@ let inline_private_constants env ((body, ctx), side_eff) = let ctx' = Univ.ContextSet.union ctx ctx' in (body, ctx') -let is_suffix l suf = match l with -| [] -> false -| _ :: l -> l == suf - (* Given the list of signatures of side effects, checks if they match. * I.e. if they are ordered descendants of the current revstruct. Returns the number of effects that can be trusted. *) -let check_signatures curmb sl = +let check_signatures senv sl = + let curmb = Certificate.make senv in let is_direct_ancestor accu mb = match accu with | None -> None - | Some (n, curmb) -> + | Some curmb -> try let mb = CEphemeron.get mb in - if is_suffix mb curmb - then Some (n + 1, mb) + if Certificate.check ~src:curmb ~dst:mb + then Some mb else None with CEphemeron.InvalidKey -> None in - let sl = List.fold_left is_direct_ancestor (Some (0, curmb)) sl in + let sl = List.fold_left is_direct_ancestor (Some curmb) sl in match sl with - | None -> 0 - | Some (n, _) -> n + | None -> None + | Some mb -> + let univs = Certificate.universes mb in + Some (Univ.ContextSet.diff univs senv.univ) type side_effect_declaration = | DefinitionEff : Entries.definition_entry -> side_effect_declaration @@ -759,13 +799,14 @@ let translate_direct_opaque env kn ce = let () = assert (is_empty_private u) in { cb with const_body = OpaqueDef c } -let export_side_effects mb env eff = +let export_side_effects senv eff = + let env = senv.env in let not_exists e = not (Environ.mem_constant e.seff_constant env) in let aux (acc,sl) e = if not (not_exists e) then acc, sl - else e :: acc, e.from_env :: sl in + else e :: acc, e.seff_certif :: sl in let seff, signatures = List.fold_left aux ([],[]) (SideEffects.repr eff) in - let trusted = check_signatures mb signatures in + let trusted = check_signatures senv signatures in let push_seff env eff = let { seff_constant = kn; seff_body = cb ; _ } = eff in let env = Environ.add_constant kn (lift_constant cb) env in @@ -774,31 +815,29 @@ let export_side_effects mb env eff = | Monomorphic ctx -> Environ.push_context_set ~strict:true ctx env in - let rec translate_seff sl seff acc env = - match seff with - | [] -> List.rev acc - | eff :: rest -> - if Int.equal sl 0 then - let env, cb = - let kn = eff.seff_constant in - let ce = constant_entry_of_side_effect eff in - let open Entries in - let cb = match ce with - | DefinitionEff ce -> - Term_typing.translate_constant env kn (DefinitionEntry ce) - | OpaqueEff ce -> - translate_direct_opaque env kn ce - in - let eff = { eff with seff_body = cb } in - (push_seff env eff, export_eff eff) - in - translate_seff 0 rest (cb :: acc) env - else - let env = push_seff env eff in - let ecb = export_eff eff in - translate_seff (sl - 1) rest (ecb :: acc) env - in - translate_seff trusted seff [] env + match trusted with + | Some univs -> + univs, List.map export_eff seff + | None -> + let rec recheck_seff seff acc env = match seff with + | [] -> List.rev acc + | eff :: rest -> + let env, cb = + let kn = eff.seff_constant in + let ce = constant_entry_of_side_effect eff in + let open Entries in + let cb = match ce with + | DefinitionEff ce -> + Term_typing.translate_constant env kn (DefinitionEntry ce) + | OpaqueEff ce -> + translate_direct_opaque env kn ce + in + let eff = { eff with seff_body = cb } in + (push_seff env eff, export_eff eff) + in + recheck_seff rest (cb :: acc) env + in + Univ.ContextSet.empty, recheck_seff seff [] env let push_opaque_proof pf senv = let o, otab = Opaqueproof.create (library_dp_of_senv senv) pf (Environ.opaque_tables senv.env) in @@ -806,7 +845,8 @@ let push_opaque_proof pf senv = senv, o let export_private_constants eff senv = - let exported = export_side_effects senv.revstruct senv.env eff in + let uctx, exported = export_side_effects senv eff in + let senv = push_context_set ~strict:true uctx senv in let map senv (kn, c) = match c.const_body with | OpaqueDef p -> let local = empty_private c.const_universes in @@ -828,7 +868,11 @@ let add_constant l decl senv = | OpaqueEntry ce -> let handle env body eff = let body, uctx, signatures = inline_side_effects env body eff in - let trusted = check_signatures senv.revstruct signatures in + let trusted = check_signatures senv signatures in + let trusted, uctx = match trusted with + | None -> 0, uctx + | Some univs -> List.length signatures, Univ.ContextSet.union univs uctx + in body, uctx, trusted in let cb, ctx = Term_typing.translate_opaque senv.env kn ce in @@ -890,9 +934,9 @@ let add_private_constant l decl senv : (Constant.t * private_constants) * safe_e in let senv = add_constant_aux senv (kn, dcb) in let eff = - let from_env = CEphemeron.create senv.revstruct in + let from_env = CEphemeron.create (Certificate.make senv) in let eff = { - from_env = from_env; + seff_certif = from_env; seff_constant = kn; seff_body = cb; } in @@ -1259,12 +1303,7 @@ let start_library dir senv = required = senv.required } let export ?except ~output_native_objects senv dir = - let senv = - try join_safe_environment ?except senv - with e -> - let e = Exninfo.capture e in - CErrors.user_err ~hdr:"export" (CErrors.iprint e) - in + let senv = join_safe_environment ?except senv in assert(senv.future_cst = []); let () = check_current_library dir senv in let mp = senv.modpath in diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index e472dfd5e5..f8d5d319a9 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/section.ml b/kernel/section.ml index 6fa0543b23..948a967f96 100644 --- a/kernel/section.ml +++ b/kernel/section.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/section.mli b/kernel/section.mli index 37d0dab317..89739c7da2 100644 --- a/kernel/section.mli +++ b/kernel/section.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 01ee91d108..466fbacca4 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/sorts.mli b/kernel/sorts.mli index fa129d10fb..49549e224d 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 11c455de73..3f81a62956 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index 9aa48bf6b4..59562f4209 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/term.ml b/kernel/term.ml index a2586e74f7..909a3ba73e 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/term.mli b/kernel/term.mli index 1fef54257a..358be59f5d 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 2ecd4880f7..c8c2301171 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -143,7 +143,7 @@ let infer_declaration env (dcl : constant_entry) = Cooking.cook_body = def; cook_type = typ; cook_universes = univs; - cook_relevance = Retypeops.relevance_of_term env j.uj_val; + cook_relevance = Relevanceops.relevance_of_term env j.uj_val; cook_inline = c.const_entry_inline_code; cook_context = c.const_entry_secctx; } diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index c9f6d66e36..3d3bdcad16 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/transparentState.ml b/kernel/transparentState.ml index 372e021c39..c2b055c30f 100644 --- a/kernel/transparentState.ml +++ b/kernel/transparentState.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/transparentState.mli b/kernel/transparentState.mli index db6d147280..da48f372ba 100644 --- a/kernel/transparentState.mli +++ b/kernel/transparentState.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 6c06c1e0f1..42fc6b2e45 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index d9842ecefa..a58d9aa50d 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 80accc1ced..19d76bfee6 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/typeops.mli b/kernel/typeops.mli index f88bc653de..e61d5c399e 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 4d15ce741c..449cd0f0f9 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index d90f01d8d1..8a8c09e911 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/uint63.mli b/kernel/uint63.mli index e0bf44da35..6b47dfc61d 100644 --- a/kernel/uint63.mli +++ b/kernel/uint63.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/uint63_31.ml b/kernel/uint63_31.ml index 445166f6af..5b2d934b5d 100644 --- a/kernel/uint63_31.ml +++ b/kernel/uint63_31.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/uint63_63.ml b/kernel/uint63_63.ml index 85b44528a7..21f57e2bfb 100644 --- a/kernel/uint63_63.ml +++ b/kernel/uint63_63.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/univ.ml b/kernel/univ.ml index 94f7076c02..0aca4b41ad 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 94e57b9efc..7651e34b12 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vars.ml b/kernel/vars.ml index c2775a6896..4c66f1574f 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vars.mli b/kernel/vars.mli index 6a1815619f..52a6159f0a 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 0a85498c40..d0f5f6804b 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vm.ml b/kernel/vm.ml index ee3e7a9913..f2d033f89b 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vm.mli b/kernel/vm.mli index 5637f7e1cd..6537d4f126 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 5acdd964b1..f4ce953d4a 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 9c24006ff0..cd85440fed 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -1,7 +1,7 @@ (************************************************************************) (* * 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) *) +(* v * Copyright INRIA, CNRS and contributors *) +(* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) |