diff options
Diffstat (limited to 'kernel')
90 files changed, 649 insertions, 427 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml index 5e1b81adc..5f683790c 100644 --- a/kernel/cClosure.ml +++ b/kernel/cClosure.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Bruno Barras with Benjamin Werner's account to implement @@ -798,7 +800,7 @@ let drop_parameters depth n argstk = s. @assumes [t] is an irreducible term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) let eta_expand_ind_stack env ind m s (f, s') = diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli index da14ff165..3a7f77d52 100644 --- a/kernel/cClosure.mli +++ b/kernel/cClosure.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -216,7 +218,7 @@ val whd_stack : s. @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive of the constructor term [c] - @raises Not_found if the inductive is not a primitive record, or if the + @raise Not_found if the inductive is not a primitive record, or if the constructor is partially applied. *) val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> diff --git a/kernel/cPrimitives.ml b/kernel/cPrimitives.ml index 14c11bf10..5b91a9b57 100644 --- a/kernel/cPrimitives.ml +++ b/kernel/cPrimitives.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) type t = diff --git a/kernel/cPrimitives.mli b/kernel/cPrimitives.mli index 8cdffb670..1e99a69d2 100644 --- a/kernel/cPrimitives.mli +++ b/kernel/cPrimitives.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) type t = diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index aa6c49bc7..5ed9b6c67 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Bruno Barras for Benjamin Grégoire as part of the @@ -32,13 +34,12 @@ let cofix_evaluated_tag = 7 let last_variant_tag = 245 type structured_constant = - | Const_sorts of Sorts.t + | Const_sort of Sorts.t | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t - | Const_type of Univ.Universe.t type reloc_table = (tag * int) array @@ -46,8 +47,8 @@ type annot_switch = {ci : case_info; rtbl : reloc_table; tailcall : bool; max_stack_size : int} let rec eq_structured_constant c1 c2 = match c1, c2 with -| Const_sorts s1, Const_sorts s2 -> Sorts.equal s1 s2 -| Const_sorts _, _ -> false +| Const_sort s1, Const_sort s2 -> Sorts.equal s1 s2 +| Const_sort _, _ -> false | Const_ind i1, Const_ind i2 -> eq_ind i1 i2 | Const_ind _, _ -> false | Const_proj p1, Const_proj p2 -> Constant.equal p1 p2 @@ -59,13 +60,11 @@ let rec eq_structured_constant c1 c2 = match c1, c2 with | Const_bn _, _ -> false | Const_univ_level l1 , Const_univ_level l2 -> Univ.Level.equal l1 l2 | Const_univ_level _ , _ -> false -| Const_type u1 , Const_type u2 -> Univ.Universe.equal u1 u2 -| Const_type _ , _ -> false let rec hash_structured_constant c = let open Hashset.Combine in match c with - | Const_sorts s -> combinesmall 1 (Sorts.hash s) + | Const_sort s -> combinesmall 1 (Sorts.hash s) | Const_ind i -> combinesmall 2 (ind_hash i) | Const_proj p -> combinesmall 3 (Constant.hash p) | Const_b0 t -> combinesmall 4 (Int.hash t) @@ -74,7 +73,6 @@ let rec hash_structured_constant c = let h = Array.fold_left fold 0 a in combinesmall 5 (combine (Int.hash t) h) | Const_univ_level l -> combinesmall 6 (Univ.Level.hash l) - | Const_type u -> combinesmall 7 (Univ.Universe.hash u) let eq_annot_switch asw1 asw2 = let eq_ci ci1 ci2 = @@ -184,6 +182,7 @@ type fv_elem = | FVnamed of Id.t | FVrel of int | FVuniv_var of int + | FVevar of Evar.t type fv = fv_elem array @@ -198,12 +197,15 @@ type t = fv_elem let compare e1 e2 = match e1, e2 with | FVnamed id1, FVnamed id2 -> Id.compare id1 id2 -| FVnamed _, _ -> -1 +| FVnamed _, (FVrel _ | FVuniv_var _ | FVevar _) -> -1 | FVrel _, FVnamed _ -> 1 | FVrel r1, FVrel r2 -> Int.compare r1 r2 -| FVrel _, FVuniv_var _ -> -1 +| FVrel _, (FVuniv_var _ | FVevar _) -> -1 | FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 -| FVuniv_var i1, _ -> 1 +| FVuniv_var i1, (FVnamed _ | FVrel _) -> 1 +| FVuniv_var i1, FVevar _ -> -1 +| FVevar _, (FVnamed _ | FVrel _ | FVuniv_var _) -> 1 +| FVevar e1, FVevar e2 -> Evar.compare e1 e2 end @@ -236,20 +238,19 @@ open Util let pp_sort s = let open Sorts in - match family s with - | InSet -> str "Set" - | InProp -> str "Prop" - | InType -> str "Type" + match s with + | Prop Null -> str "Prop" + | Prop Pos -> str "Set" + | Type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let rec pp_struct_const = function - | Const_sorts s -> pp_sort s + | Const_sort s -> pp_sort s | Const_ind (mind, i) -> MutInd.print mind ++ str"#" ++ int i | Const_proj p -> Constant.print p | Const_b0 i -> int i | Const_bn (i,t) -> int i ++ surround (prvect_with_sep pr_comma pp_struct_const t) | Const_univ_level l -> Univ.Level.pr l - | Const_type u -> str "Type@{" ++ Univ.pr_uni u ++ str "}" let pp_lbl lbl = str "L" ++ int lbl @@ -257,6 +258,7 @@ let pp_fv_elem = function | FVnamed id -> str "FVnamed(" ++ Id.print id ++ str ")" | FVrel i -> str "Rel(" ++ int i ++ str ")" | FVuniv_var v -> str "FVuniv(" ++ int v ++ str ")" + | FVevar e -> str "FVevar(" ++ int (Evar.repr e) ++ str ")" let rec pp_instr i = match i with diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index c8fbb27a9..03b6bc619 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* $Id$ *) @@ -26,13 +28,12 @@ val cofix_evaluated_tag : tag val last_variant_tag : tag type structured_constant = - | Const_sorts of Sorts.t + | Const_sort of Sorts.t | Const_ind of inductive | Const_proj of Constant.t | Const_b0 of tag | Const_bn of tag * structured_constant array | Const_univ_level of Univ.Level.t - | Const_type of Univ.Universe.t val pp_struct_const : structured_constant -> Pp.t @@ -138,6 +139,7 @@ type fv_elem = FVnamed of Id.t | FVrel of int | FVuniv_var of int +| FVevar of Evar.t type fv = fv_elem array diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 3104d5751..0766f49b3 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction @@ -257,6 +259,15 @@ let pos_universe_var i r sz = r.in_env := push_fv db env; Kenvacc(r.offset + pos) +let pos_evar evk r = + let env = !(r.in_env) in + let cid = FVevar evk in + try Kenvacc(r.offset + find_at cid env) + with Not_found -> + let pos = env.size in + r.in_env := push_fv cid env; + Kenvacc (r.offset + pos) + (*i Examination of the continuation *) (* Discard all instructions up to the next label. *) @@ -427,6 +438,7 @@ let compile_fv_elem reloc fv sz cont = | FVrel i -> pos_rel i reloc sz :: cont | FVnamed id -> pos_named id reloc :: cont | FVuniv_var i -> pos_universe_var i reloc sz :: cont + | FVevar evk -> pos_evar evk reloc :: cont let rec compile_fv reloc l sz cont = match l with @@ -471,6 +483,12 @@ let rec compile_lam env reloc lam sz cont = | Lvar id -> pos_named id reloc :: cont + | Levar (evk, args) -> + if Array.is_empty args then + compile_fv_elem reloc (FVevar evk) sz cont + else + comp_app compile_fv_elem (compile_lam env) reloc (FVevar evk) args sz cont + | Lconst (kn,u) -> compile_constant env reloc kn u [||] sz cont | Lind (ind,u) -> @@ -480,23 +498,23 @@ let rec compile_lam env reloc lam sz cont = (Const_ind ind) (Univ.Instance.to_array u) sz cont | Lsort (Sorts.Prop _ as s) -> - compile_structured_constant reloc (Const_sorts s) sz cont + compile_structured_constant reloc (Const_sort s) sz cont | Lsort (Sorts.Type u) -> - (* We separate global and local universes in [u]. The former will be part - of the structured constant, while the later (if any) will be applied as - arguments. *) - let open Univ in begin + (* We separate global and local universes in [u]. The former will be part + of the structured constant, while the later (if any) will be applied as + arguments. *) + let open Univ in begin let u,s = Universe.compact u in (* We assume that [Universe.type0m] is a neutral element for [Universe.sup] *) + let compile_get_univ reloc idx sz cont = + set_max_stack_size sz; + compile_fv_elem reloc (FVuniv_var idx) sz cont + in if List.is_empty s then - compile_structured_constant reloc (Const_sorts (Sorts.Type u)) sz cont + compile_structured_constant reloc (Const_sort (Sorts.Type u)) sz cont else - let compile_get_univ reloc idx sz cont = - set_max_stack_size sz; - compile_fv_elem reloc (FVuniv_var idx) sz cont - in comp_app compile_structured_constant compile_get_univ reloc - (Const_type u) (Array.of_list s) sz cont + (Const_sort (Sorts.Type u)) (Array.of_list s) sz cont end | Llet (id,def,body) -> diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli index 99f2a3c01..abab58b60 100644 --- a/kernel/cbytegen.mli +++ b/kernel/cbytegen.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Cbytecodes diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 856b0b465..14f4f27c0 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction @@ -350,7 +352,7 @@ type to_patch = emitcodes * patches * fv (* Substitution *) let rec subst_strcst s sc = match sc with - | Const_sorts _ | Const_b0 _ | Const_univ_level _ | Const_type _ -> sc + | Const_sort _ | Const_b0 _ | Const_univ_level _ -> sc | Const_proj p -> Const_proj (subst_constant s p) | Const_bn(tag,args) -> Const_bn(tag,Array.map (subst_strcst s) args) | Const_ind ind -> let kn,i = ind in Const_ind (subst_mind s kn, i) diff --git a/kernel/cinstr.mli b/kernel/cinstr.mli index 2d9ec6050..4a3c03d85 100644 --- a/kernel/cinstr.mli +++ b/kernel/cinstr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Constr @@ -20,6 +22,7 @@ type uint = and lambda = | Lrel of Name.t * int | Lvar of Id.t + | Levar of Evar.t * lambda array | Lprod of lambda * lambda | Llam of Name.t array * lambda | Llet of Name.t * lambda * lambda diff --git a/kernel/clambda.ml b/kernel/clambda.ml index 636ed3510..7b637c20e 100644 --- a/kernel/clambda.ml +++ b/kernel/clambda.ml @@ -29,6 +29,9 @@ let rec pp_lam lam = match lam with | Lrel (id,n) -> pp_rel id n | Lvar id -> Id.print id + | Levar (evk, args) -> + hov 1 (str "evar(" ++ Evar.print evk ++ str "," ++ spc () ++ + prlist_with_sep spc pp_lam (Array.to_list args) ++ str ")") | Lprod(dom,codom) -> hov 1 (str "forall(" ++ pp_lam dom ++ @@ -148,6 +151,9 @@ let shift subst = subs_shft (1, subst) let rec map_lam_with_binders g f n lam = match lam with | Lrel _ | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> lam + | Levar (evk, args) -> + let args' = Array.smartmap (f n) args in + if args == args' then lam else Levar (evk, args') | Lprod(dom,codom) -> let dom' = f n dom in let codom' = f n codom in @@ -344,6 +350,8 @@ let rec occurrence k kind lam = if kind then false else raise Not_found else kind | Lvar _ | Lconst _ | Lval _ | Lsort _ | Lind _ -> kind + | Levar (_, args) -> + occurrence_args k kind args | Lprod(dom, codom) -> occurrence k (occurrence k kind dom) codom | Llam(ids,body) -> @@ -600,7 +608,9 @@ open Renv let rec lambda_of_constr env c = match Constr.kind c with | Meta _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr: Meta") - | Evar _ -> raise (Invalid_argument "Cbytegen.lambda_of_constr : Evar") + | Evar (evk, args) -> + let args = lambda_of_args env 0 args in + Levar (evk, args) | Cast (c, _, _) -> lambda_of_constr env c diff --git a/kernel/constr.ml b/kernel/constr.ml index 1ff1fcc4c..2cbcdd76e 100644 --- a/kernel/constr.ml +++ b/kernel/constr.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* File initially created by Gérard Huet and Thierry Coquand in 1984 *) diff --git a/kernel/constr.mli b/kernel/constr.mli index 19ffa8fe3..f7e4eecba 100644 --- a/kernel/constr.mli +++ b/kernel/constr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines the most important datatype of Coq, namely kernel terms, diff --git a/kernel/context.ml b/kernel/context.ml index d635c4515..4f3f649c1 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre out of names.ml as part of the diff --git a/kernel/context.mli b/kernel/context.mli index c3ecd8d4e..c97db4348 100644 --- a/kernel/context.mli +++ b/kernel/context.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** The modules defined below represent a {e local context} diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index ca568fc6e..7ef63c186 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Bruno Barras as part of the rewriting of the conversion diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 02c179ab6..67add5dd3 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/cooking.ml b/kernel/cooking.ml index 23a578d99..6f4541e95 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre out of V6.3 file constants.ml diff --git a/kernel/cooking.mli b/kernel/cooking.mli index 7696d7545..7bd0ae566 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 236d83576..012948954 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Bruno Barras for Benjamin Grégoire as part of the @@ -150,6 +152,7 @@ and slot_for_fv env fv = env |> Pre_env.lookup_rel i |> RelDecl.get_value |> fill_fv_cache rv i val_of_rel env_of_rel | Some (v, _) -> v end + | FVevar evk -> val_of_evar evk | FVuniv_var idu -> assert false diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli index fc935f6ee..19b2b8b50 100644 --- a/kernel/csymtable.mli +++ b/kernel/csymtable.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* $Id$ *) diff --git a/kernel/declarations.ml b/kernel/declarations.ml index cb7f0ecef..b7427d20a 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/declareops.ml b/kernel/declareops.ml index 9eed9efcb..3652a1ce4 100644 --- a/kernel/declareops.ml +++ b/kernel/declareops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Declarations diff --git a/kernel/declareops.mli b/kernel/declareops.mli index 0eed11f49..fb46112ea 100644 --- a/kernel/declareops.mli +++ b/kernel/declareops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Declarations diff --git a/kernel/entries.ml b/kernel/entries.ml index 36b75668b..94da00c7e 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/environ.ml b/kernel/environ.ml index fe5a7dfb5..9d4063e43 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Author: Jean-Christophe Filliâtre as part of the rebuilding of Coq diff --git a/kernel/environ.mli b/kernel/environ.mli index 69d811a64..4e6ac1e72 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -199,7 +201,7 @@ val lookup_modtype : ModPath.t -> env -> module_type_body (** {5 Universe constraints } *) (** Add universe constraints to the environment. - @raises UniverseInconsistency + @raise UniverseInconsistency . *) val add_constraints : Univ.Constraint.t -> env -> env diff --git a/kernel/esubst.ml b/kernel/esubst.ml index ac2b3f9d5..a11a0dc00 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Bruno Barras for Coq V7.0, Mar 2001 *) diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 95a2e71c2..b82d6fdf0 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Explicit substitutions *) diff --git a/kernel/evar.ml b/kernel/evar.ml index dcd2e12a0..bbe143092 100644 --- a/kernel/evar.ml +++ b/kernel/evar.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) type t = int diff --git a/kernel/evar.mli b/kernel/evar.mli index 6a058207f..d14cdce27 100644 --- a/kernel/evar.mli +++ b/kernel/evar.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This module defines existential variables, which are isomorphic to [int]. diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index cfca335d3..439acd15b 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 9a9380adb..5a38172c2 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 722705bd7..9bed598bb 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors @@ -1067,6 +1069,9 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = try find_inductive env a with Not_found -> raise_err env i (RecursionNotOnInductiveType a) in + let mib,_ = lookup_mind_specif env (out_punivs mind) in + if mib.mind_finite != Finite then + raise_err env i (RecursionNotOnInductiveType a); (mind, (env', b)) else check_occur env' (n+1) b else anomaly ~label:"check_one_fix" (Pp.str "Bad occurrence of recursive call.") diff --git a/kernel/inductive.mli b/kernel/inductive.mli index 8aaeee831..c7982f1fc 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 2c8ef477f..9c2fa0546 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Claudio Sacerdoti from contents of term.ml, names.ml and diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index 1aa7ba519..b14d39207 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** {6 [Mod_subst] } *) diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index 6b89a1da0..1baab7c98 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 1225c3e1e..e74f455ef 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Declarations diff --git a/kernel/modops.ml b/kernel/modops.ml index 11e6be659..bbf160db2 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/modops.mli b/kernel/modops.mli index bbb4c918c..cb41a5123 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/names.ml b/kernel/names.ml index b02c0b840..6fa44c061 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* File created around Apr 1994 for CiC V5.10.5 by Chet Murthy collecting diff --git a/kernel/names.mli b/kernel/names.mli index b1e8efd8d..209826c1f 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) (** This file defines a lot of different notions of names used pervasively in diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml index 8fa254053..c82d982b4 100644 --- a/kernel/nativecode.ml +++ b/kernel/nativecode.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/nativecode.mli b/kernel/nativecode.mli index 7d20054f7..4b23cc5f8 100644 --- a/kernel/nativecode.mli +++ b/kernel/nativecode.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Constr diff --git a/kernel/nativeconv.ml b/kernel/nativeconv.ml index bfa982136..c71f746be 100644 --- a/kernel/nativeconv.ml +++ b/kernel/nativeconv.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli index 769deacae..2111739d5 100644 --- a/kernel/nativeconv.mli +++ b/kernel/nativeconv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr open Reduction diff --git a/kernel/nativeinstr.mli b/kernel/nativeinstr.mli index 48ad88444..9c17cc2b5 100644 --- a/kernel/nativeinstr.mli +++ b/kernel/nativeinstr.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Constr diff --git a/kernel/nativelambda.ml b/kernel/nativelambda.ml index dfe9d025e..01ddffe3e 100644 --- a/kernel/nativelambda.ml +++ b/kernel/nativelambda.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Names diff --git a/kernel/nativelambda.mli b/kernel/nativelambda.mli index 933fbc660..9a1e19b3c 100644 --- a/kernel/nativelambda.mli +++ b/kernel/nativelambda.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Constr diff --git a/kernel/nativelib.ml b/kernel/nativelib.ml index 1e35f6c03..31ad36491 100644 --- a/kernel/nativelib.ml +++ b/kernel/nativelib.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util open Nativevalues diff --git a/kernel/nativelib.mli b/kernel/nativelib.mli index b74d4fdd0..25adcf224 100644 --- a/kernel/nativelib.mli +++ b/kernel/nativelib.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Nativecode diff --git a/kernel/nativelibrary.ml b/kernel/nativelibrary.ml index c68f78121..c69cf722b 100644 --- a/kernel/nativelibrary.ml +++ b/kernel/nativelibrary.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/nativelibrary.mli b/kernel/nativelibrary.mli index 72e3d8041..31e5255fc 100644 --- a/kernel/nativelibrary.mli +++ b/kernel/nativelibrary.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Declarations diff --git a/kernel/nativevalues.ml b/kernel/nativevalues.ml index 3d47b1672..cfcb0a485 100644 --- a/kernel/nativevalues.ml +++ b/kernel/nativevalues.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/kernel/nativevalues.mli b/kernel/nativevalues.mli index 993842740..4a58a3c7d 100644 --- a/kernel/nativevalues.mli +++ b/kernel/nativevalues.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr open Names diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml index c2fcfbfd6..a484c08e8 100644 --- a/kernel/opaqueproof.ml +++ b/kernel/opaqueproof.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli index c8339e6eb..b6ae80b46 100644 --- a/kernel/opaqueproof.mli +++ b/kernel/opaqueproof.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index 6c5e1cde5..8ebe48e20 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Benjamin Grégoire out of environ.ml for better diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index a6b57bd1b..b05074814 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/reduction.ml b/kernel/reduction.ml index aba2b5535..2e59fcc18 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created under Benjamin Werner account by Bruno Barras to implement @@ -267,8 +269,9 @@ let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u if not (Int.equal num_cnstr_args nargs) then cmp_instances u1 u2 s else - let csts = get_cumulativity_constraints CONV cumi u1 u2 in - cmp_cumul csts s + (** By invariant, both constructors have a common supertype, + so they are convertible _at that type_. *) + s let convert_constructors ctor nargs u1 u2 (s, check) = convert_constructors_gen (check.compare_instances ~flex:false) check.compare_cumul_instances diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 6f7e3f8f8..ad52c93f6 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 24d022d69..d76b05a8b 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Arnaud Spiwack, May 2007 *) diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 134b4b4f7..0334e7a9e 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 93b8e278f..de2a890fb 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Jean-Christophe Filliâtre as part of the rebuilding of diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 757b803a3..4078a9092 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/sorts.ml b/kernel/sorts.ml index 07688840d..daeb90be7 100644 --- a/kernel/sorts.ml +++ b/kernel/sorts.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ diff --git a/kernel/sorts.mli b/kernel/sorts.mli index 65ea75138..1bbde2608 100644 --- a/kernel/sorts.mli +++ b/kernel/sorts.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** {6 The sorts of CCI. } *) diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index e95d5d2b5..8cf588c3e 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index 67df3759e..4e755e42f 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ diff --git a/kernel/term.ml b/kernel/term.ml index a4c92bd33..403ed881c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Util diff --git a/kernel/term.mli b/kernel/term.mli index b4597676a..ba521978e 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 9b864440d..e621a61c7 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created by Jacek Chrzaszcz, Aug 2002 as part of the implementation of diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 7bc029010..6a0ff072f 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 781c6bfbc..1c323e3ea 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 72861f6e4..20bf300ac 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 4a935f581..be4c0e1ec 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open CErrors diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 5584b6ab4..bff40b017 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index f1e8d1031..5d1644614 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -833,7 +835,7 @@ let sort_universes g = (** Subtyping of polymorphic contexts *) let check_subtype univs ctxT ctx = - if AUContext.size ctx == AUContext.size ctx then + if AUContext.size ctxT == AUContext.size ctx then let (inst, cst) = UContext.dest (AUContext.repr ctx) in let cstT = UContext.constraints (AUContext.repr ctxT) in let push accu v = add_universe v false accu in diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli index f71d83d85..d4fba63fb 100644 --- a/kernel/uGraph.mli +++ b/kernel/uGraph.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Univ @@ -41,7 +43,7 @@ val check_constraint : t -> univ_constraint -> bool val check_constraints : Constraint.t -> t -> bool (** Adds a universe to the graph, ensuring it is >= or > Set. - @raises AlreadyDeclared if the level is already declared in the graph. *) + @raise AlreadyDeclared if the level is already declared in the graph. *) exception AlreadyDeclared diff --git a/kernel/univ.ml b/kernel/univ.ml index c42b66749..584593e2f 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (* Created in Caml by Gérard Huet for CoC 4.8 [Dec 1988] *) diff --git a/kernel/univ.mli b/kernel/univ.mli index 74d1bfd3a..ce617932c 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * 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) *) (************************************************************************) (** Universes. *) diff --git a/kernel/vars.ml b/kernel/vars.ml index b3b3eff62..0f588a630 100644 --- a/kernel/vars.ml +++ b/kernel/vars.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -310,6 +312,3 @@ let subst_instance_constr subst c = let subst_instance_context s ctx = if Univ.Instance.is_empty s then ctx else Context.Rel.map (fun x -> subst_instance_constr s x) ctx - -type id_key = Constant.t tableKey -let eq_id_key x y = Names.eq_table_key Constant.equal x y diff --git a/kernel/vars.mli b/kernel/vars.mli index b74d25260..a0c7ba4bd 100644 --- a/kernel/vars.mli +++ b/kernel/vars.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -137,6 +139,3 @@ val subst_univs_level_context : Univ.universe_level_subst -> Context.Rel.t -> Co (** Instance substitution for polymorphism. *) val subst_instance_constr : Instance.t -> constr -> constr val subst_instance_context : Instance.t -> Context.Rel.t -> Context.Rel.t - -type id_key = Constant.t tableKey -val eq_id_key : id_key -> id_key -> bool diff --git a/kernel/vconv.ml b/kernel/vconv.ml index 8c7658147..f11803b67 100644 --- a/kernel/vconv.ml +++ b/kernel/vconv.ml @@ -44,7 +44,6 @@ let rec conv_val env pb k v1 v2 cu = and conv_whd env pb k whd1 whd2 cu = (* Pp.(msg_debug (str "conv_whd(" ++ pr_whd whd1 ++ str ", " ++ pr_whd whd2 ++ str ")")) ; *) match whd1, whd2 with - | Vsort s1, Vsort s2 -> sort_cmp_universes env pb s1 s2 cu | Vuniv_level _ , _ | _ , Vuniv_level _ -> (** Both of these are invalid since universes are handled via @@ -81,7 +80,7 @@ and conv_whd env pb k whd1 whd2 cu = (* on the fly eta expansion *) conv_val env CONV (k+1) (apply_whd k whd1) (apply_whd k whd2) cu - | Vsort _, _ | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ + | Vprod _, _ | Vfix _, _ | Vcofix _, _ | Vconstr_const _, _ | Vconstr_block _, _ | Vatom_stk _, _ -> raise NotConvertible @@ -116,11 +115,12 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu = conv_stack env k stk1 stk2 cu else raise NotConvertible | Aid ik1, Aid ik2 -> - if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then + if Vmvalues.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then conv_stack env k stk1 stk2 cu else raise NotConvertible - | Atype _ , _ | _, Atype _ -> assert false - | Aind _, _ | Aid _, _ -> raise NotConvertible + | Asort s1, Asort s2 -> + sort_cmp_universes env pb s1 s2 cu + | Asort _ , _ | Aind _, _ | Aid _, _ -> raise NotConvertible and conv_stack env k stk1 stk2 cu = match stk1, stk2 with diff --git a/kernel/vconv.mli b/kernel/vconv.mli index c3c9636e8..620f6b5e8 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Constr diff --git a/kernel/vm.ml b/kernel/vm.ml index 352ea74a4..14aeb732f 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Cbytecodes @@ -28,7 +30,6 @@ let popstop_code i = let stop = popstop_code 0 - (************************************************) (* Abstract machine *****************************) (************************************************) @@ -70,7 +71,6 @@ let apply_varray vf varray = interprete (fun_code vf) (fun_val vf) (fun_env vf) (n - 1) end -(* Functions over vfun *) let mkrel_vstack k arity = let max = k + arity - 1 in Array.init arity (fun i -> val_of_rel (max - i)) @@ -168,7 +168,7 @@ let rec apply_stack a stk v = let apply_whd k whd = let v = val_of_rel k in match whd with - | Vsort _ | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false + | Vprod _ | Vconstr_const _ | Vconstr_block _ -> assert false | Vfun f -> reduce_fun k f | Vfix(f, None) -> push_ra stop; diff --git a/kernel/vm.mli b/kernel/vm.mli index c6d92ba26..50ebc9062 100644 --- a/kernel/vm.mli +++ b/kernel/vm.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Vmvalues diff --git a/kernel/vmvalues.ml b/kernel/vmvalues.ml index 2d8a1d976..0e0cb4e58 100644 --- a/kernel/vmvalues.ml +++ b/kernel/vmvalues.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names open Sorts @@ -118,10 +120,23 @@ type vswitch = { (* Do not edit this type without editing C code, especially "coq_values.h" *) +type id_key = +| ConstKey of Constant.t +| VarKey of Id.t +| RelKey of Int.t +| EvarKey of Evar.t + +let eq_id_key k1 k2 = match k1, k2 with +| ConstKey c1, ConstKey c2 -> Constant.equal c1 c2 +| VarKey id1, VarKey id2 -> Id.equal id1 id2 +| RelKey n1, RelKey n2 -> Int.equal n1 n2 +| EvarKey evk1, EvarKey evk2 -> Evar.equal evk1 evk2 +| _ -> false + type atom = - | Aid of Vars.id_key + | Aid of id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (* Zippers *) @@ -136,7 +151,6 @@ type stack = zipper list type to_update = values type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -167,7 +181,6 @@ let uni_lvl_val (v : values) : Univ.Level.t = let pr = let open Pp in match whd with - | Vsort _ -> str "Vsort" | Vprod _ -> str "Vprod" | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" @@ -189,12 +202,17 @@ let rec whd_accu a stk = match Obj.tag at with | i when Int.equal i type_atom_tag -> begin match stk with + | [] -> Vatom_stk(Obj.magic at, stk) | [Zapp args] -> let args = Array.init (nargs args) (arg args) in - let u = Obj.obj (Obj.field at 0) in - let inst = Instance.of_array (Array.map uni_lvl_val args) in - let u = Univ.subst_instance_universe inst u in - Vsort (Type u) + let s = Obj.obj (Obj.field at 0) in + begin match s with + | Type u -> + let inst = Instance.of_array (Array.map uni_lvl_val args) in + let u = Univ.subst_instance_universe inst u in + Vatom_stk (Asort (Type u), []) + | _ -> assert false + end | _ -> assert false end | i when i <= max_atom_tag -> @@ -243,11 +261,8 @@ let whd_val : values -> whd = else let tag = Obj.tag o in if tag = accu_tag then - ( - if Int.equal (Obj.size o) 1 then Obj.obj o (* sort *) - else - if is_accumulate (fun_code o) then whd_accu o [] - else Vprod(Obj.obj o)) + if is_accumulate (fun_code o) then whd_accu o [] + else Vprod(Obj.obj o) else if tag = Obj.closure_tag || tag = Obj.infix_tag then (match kind_of_closure o with @@ -273,7 +288,7 @@ let obj_of_atom : atom -> Obj.t = (* obj_of_str_const : structured_constant -> Obj.t *) let rec obj_of_str_const str = match str with - | Const_sorts s -> Obj.repr (Vsort s) + | Const_sort s -> obj_of_atom (Asort s) | Const_ind ind -> obj_of_atom (Aind ind) | Const_proj p -> Obj.repr p | Const_b0 tag -> Obj.repr tag @@ -285,7 +300,6 @@ let rec obj_of_str_const str = done; res | Const_univ_level l -> Obj.repr (Vuniv_level l) - | Const_type u -> obj_of_atom (Atype u) let val_of_obj o = ((Obj.obj o) : values) @@ -304,13 +318,14 @@ let val_of_proj kn v = module IdKeyHash = struct - type t = Constant.t tableKey - let equal = Names.eq_table_key Constant.equal + type t = id_key + let equal = eq_id_key open Hashset.Combine let hash = function | ConstKey c -> combinesmall 1 (Constant.hash c) | VarKey id -> combinesmall 2 (Id.hash id) | RelKey i -> combinesmall 3 (Int.hash i) + | EvarKey evk -> combinesmall 4 (Evar.hash evk) end module KeyTable = Hashtbl.Make(IdKeyHash) @@ -330,6 +345,8 @@ let val_of_named id = val_of_idkey (VarKey id) let val_of_constant c = val_of_idkey (ConstKey c) +let val_of_evar evk = val_of_idkey (EvarKey evk) + external val_of_annot_switch : annot_switch -> values = "%identity" (*************************************************) @@ -502,10 +519,9 @@ let rec pr_atom a = | RelKey i -> str "#" ++ int i | _ -> str "...") ++ str ")" | Aind (mi,i) -> str "Aind(" ++ MutInd.print mi ++ str "#" ++ int i ++ str ")" - | Atype _ -> str "Atype(") + | Asort _ -> str "Asort(") and pr_whd w = Pp.(match w with - | Vsort _ -> str "Vsort" | Vprod _ -> str "Vprod" | Vfun _ -> str "Vfun" | Vfix _ -> str "Vfix" diff --git a/kernel/vmvalues.mli b/kernel/vmvalues.mli index 350f71372..c6e342a96 100644 --- a/kernel/vmvalues.mli +++ b/kernel/vmvalues.mli @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Names @@ -54,10 +56,18 @@ val fun_code : vfun -> tcode val fix_code : vfix -> tcode val cofix_upd_code : to_update -> tcode +type id_key = +| ConstKey of Constant.t +| VarKey of Id.t +| RelKey of Int.t +| EvarKey of Evar.t + +val eq_id_key : id_key -> id_key -> bool + type atom = - | Aid of Vars.id_key + | Aid of id_key | Aind of inductive - | Atype of Univ.Universe.t + | Asort of Sorts.t (** Zippers *) @@ -70,7 +80,6 @@ type zipper = type stack = zipper list type whd = - | Vsort of Sorts.t | Vprod of vprod | Vfun of vfun | Vfix of vfix * arguments option @@ -92,6 +101,7 @@ val val_of_str_const : structured_constant -> values val val_of_rel : int -> values val val_of_named : Id.t -> values val val_of_constant : Constant.t -> values +val val_of_evar : Evar.t -> values val val_of_proj : Constant.t -> values -> values val val_of_atom : atom -> values |