diff options
| author |  Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
| commit | 300293c119981054c95182a90c829058530a6b6f (patch) | |
| tree | d7303613741c5796b58ced7db24ec7203327dbb2 /kernel | |
| parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) | |
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'kernel')
55 files changed, 186 insertions, 290 deletions
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c index cce2319b..a0cb4f1a 100644 --- a/kernel/byterun/coq_interp.c +++ b/kernel/byterun/coq_interp.c @@ -145,7 +145,7 @@ sp is a local copy of the global variable extern_sp. */ #define SP_REG asm("a4") #define ACCU_REG asm("d7") #endif -#ifdef __arm__ +#if defined(__arm__) && !defined(__thumb2__) #define PC_REG asm("r9") #define SP_REG asm("r8") #define ACCU_REG asm("r7") diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 4a9c7da2..0b4df194 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -295,6 +295,8 @@ let init () = type emitcodes = string +let copy = String.copy + let length = String.length type to_patch = emitcodes * (patch list) * fv @@ -341,6 +343,8 @@ let is_boxed tps = | BCdefined(b,_) -> b | _ -> false +let repr_body_code = repr_substituted + let to_memory (init_code, fun_code, fv) = init(); emit init_code; diff --git a/kernel/cemitcodes.mli b/kernel/cemitcodes.mli index 965228fa..384146d2 100644 --- a/kernel/cemitcodes.mli +++ b/kernel/cemitcodes.mli @@ -12,6 +12,8 @@ val subst_patch : Mod_subst.substitution -> patch -> patch type emitcodes +val copy : emitcodes -> emitcodes + val length : emitcodes -> int val patch_int : emitcodes -> (*pos*)int -> int -> unit @@ -36,5 +38,8 @@ val is_boxed : to_patch_substituted -> bool val subst_to_patch_subst : Mod_subst.substitution -> to_patch_substituted -> to_patch_substituted +val repr_body_code : + to_patch_substituted -> Mod_subst.substitution list option * body_code + val to_memory : bytecodes * bytecodes * fv -> to_patch (* init code, fun code, fv *) diff --git a/kernel/closure.ml b/kernel/closure.ml index 3f4c1059..bb68835e 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: closure.ml 13340 2010-07-28 12:22:04Z barras $ *) +(* $Id: closure.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Pp diff --git a/kernel/closure.mli b/kernel/closure.mli index 0af30bed..9cfd9797 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: closure.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: closure.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Pp diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 935f6fe7..3f6b77b0 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: conv_oracle.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: conv_oracle.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Names diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index 94911edd..9272dfe5 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: conv_oracle.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: conv_oracle.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Names diff --git a/kernel/cooking.ml b/kernel/cooking.ml index ad5e725b..d35c011a 100644 --- a/kernel/cooking.ml +++ b/kernel/cooking.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cooking.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: cooking.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Pp open Util diff --git a/kernel/cooking.mli b/kernel/cooking.mli index bd1f4aec..df7e51f2 100644 --- a/kernel/cooking.mli +++ b/kernel/cooking.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: cooking.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: cooking.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) open Names open Term diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 8eeb1ce6..2b3d3fac 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -81,9 +81,10 @@ let annot_tbl = Hashtbl.create 31 exception NotEvaluated +open Pp let key rk = match !rk with - | Some k -> k + | Some k -> (*Pp.msgnl (str"found at: "++int k);*) k | _ -> raise NotEvaluated (************************) @@ -110,6 +111,7 @@ let rec slot_for_getglobal env kn = let (cb,rk) = lookup_constant_key kn env in try key rk with NotEvaluated -> +(* Pp.msgnl(str"not yet evaluated");*) let pos = match Cemitcodes.force cb.const_body_code with | BCdefined(boxed,(code,pl,fv)) -> @@ -118,6 +120,7 @@ let rec slot_for_getglobal env kn = else set_global v | BCallias kn' -> slot_for_getglobal env kn' | BCconstant -> set_global (val_of_constant kn) in +(*Pp.msgnl(str"value stored at: "++int pos);*) rk := Some pos; pos @@ -154,15 +157,22 @@ and slot_for_fv env fv = end and eval_to_patch env (buff,pl,fv) = + (* copy code *before* patching because of nested evaluations: + the code we are patching might be called (and thus "concurrently" patched) + and results in wrong results. Side-effects... *) + let buff = Cemitcodes.copy buff in let patch = function | Reloc_annot a, pos -> patch_int buff pos (slot_for_annot a) | Reloc_const sc, pos -> patch_int buff pos (slot_for_str_cst sc) | Reloc_getglobal kn, pos -> - patch_int buff pos (slot_for_getglobal env kn) +(* Pp.msgnl (str"patching global: "++str(debug_string_of_con kn));*) + patch_int buff pos (slot_for_getglobal env kn); +(* Pp.msgnl (str"patch done: "++str(debug_string_of_con kn))*) in List.iter patch pl; let vm_env = Array.map (slot_for_fv env) fv in let tc = tcode_of_code buff (length buff) in +(*Pp.msgnl (str"execute code");*) eval_tcode tc vm_env and val_of_constr env c = diff --git a/kernel/declarations.ml b/kernel/declarations.ml index 42055a23..c18e6bb0 100644 --- a/kernel/declarations.ml +++ b/kernel/declarations.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: declarations.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/kernel/declarations.mli b/kernel/declarations.mli index ee1242bb..db706a0c 100644 --- a/kernel/declarations.mli +++ b/kernel/declarations.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declarations.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: declarations.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/entries.ml b/kernel/entries.ml index cec46423..4ca21277 100644 --- a/kernel/entries.ml +++ b/kernel/entries.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: entries.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: entries.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/entries.mli b/kernel/entries.mli index ecc50213..d71b48f6 100644 --- a/kernel/entries.mli +++ b/kernel/entries.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: entries.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: entries.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/environ.ml b/kernel/environ.ml index 935faae6..e6fafce9 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: environ.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: environ.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names @@ -516,144 +516,3 @@ fun env field value -> in Retroknowledge.add_field retroknowledge_with_reactive_info field value } - - -(**************************************************************) -(* spiwack: the following definitions are used by the function - [assumptions] which gives as an output the set of all - axioms and sections variables on which a given term depends - in a context (expectingly the Global context) *) - -type context_object = - | Variable of identifier (* A section variable or a Let definition *) - | Axiom of constant (* An axiom or a constant. *) - | Opaque of constant (* An opaque constant. *) - -(* Defines a set of [assumption] *) -module OrderedContextObject = -struct - type t = context_object - let compare x y = - match x , y with - | Variable i1 , Variable i2 -> id_ord i1 i2 - | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2 - (* spiwack: it would probably be cleaner - to provide a [kn_ord] function *) - | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2 - | Variable _ , Axiom _ -> -1 - | Axiom _ , Variable _ -> 1 - | Opaque _ , _ -> -1 - | _, Opaque _ -> 1 -end - -module ContextObjectSet = Set.Make (OrderedContextObject) -module ContextObjectMap = Map.Make (OrderedContextObject) - - -let assumptions ?(add_opaque=false) st (* t env *) = - let (idts,knst) = st in - (* Infix definition for chaining function that accumulate - on a and a ContextObjectSet, ContextObjectMap. *) - let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in - (* This function eases memoization, by checking if an object is already - stored before trying and applying a function. - If the object is there, the function is not fired (we are in a - particular case where memoized object don't need a treatment at all). - If the object isn't there, it is stored and the function is fired*) - let try_and_go o f s m = - if ContextObjectSet.mem o s then - (s,m) - else - f (ContextObjectSet.add o s) m - in - let identity2 s m = (s,m) in - (* Goes recursively into the term to see if it depends on assumptions - the 3 important cases are : - Const _ where we need to first unfold - the constant and return the needed assumptions of its body in the - environment, - - Rel _ which means the term is a variable - which has been bound earlier by a Lambda or a Prod (returns [] ), - - Var _ which means that the term refers - to a section variable or a "Let" definition, in the former it is - an assumption of [t], in the latter is must be unfolded like a Const. - The other cases are straightforward recursion. - Calls to the environment are memoized, thus avoiding to explore - the DAG of the environment as if it was a tree (can cause - exponential behavior and prevent the algorithm from terminating - in reasonable time). [s] is a set of [context_object], representing - the object already visited.*) - let rec aux t env s acc = - match kind_of_term t with - | Var id -> aux_memoize_id id env s acc - | Meta _ | Evar _ -> - Util.anomaly "Environ.assumption: does not expect a meta or an evar" - | Cast (e1,_,e2) | Prod (_,e1,e2) | Lambda (_,e1,e2) -> - ((aux e1 env)**(aux e2 env)) s acc - | LetIn (_,e1,e2,e3) -> ((aux e1 env)** - (aux e2 env)** - (aux e3 env)) - s acc - | App (e1, e_array) -> ((aux e1 env)** - (Array.fold_right - (fun e f -> (aux e env)**f) - e_array identity2)) - s acc - | Case (_,e1,e2,e_array) -> ((aux e1 env)** - (aux e2 env)** - (Array.fold_right - (fun e f -> (aux e env)**f) - e_array identity2)) - s acc - | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> - ((Array.fold_right - (fun e f -> (aux e env)**f) - e1_array identity2) ** - (Array.fold_right - (fun e f -> (aux e env)**f) - e2_array identity2)) - s acc - | Const kn -> aux_memoize_kn kn env s acc - | _ -> (s,acc) (* closed atomic types + rel *) - - and add_id id env s acc = - (* a Var can be either a variable, or a "Let" definition.*) - match lookup_named id env with - | (_,None,t) -> - (s,ContextObjectMap.add (Variable id) t acc) - | (_,Some bdy,_) -> aux bdy env s acc - - and aux_memoize_id id env = - try_and_go (Variable id) (add_id id env) - - and add_kn kn env s acc = - let cb = lookup_constant kn env in - let do_type cst = - let ctype = - match cb.Declarations.const_type with - | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level) - | NonPolymorphicType t -> t - in - (s,ContextObjectMap.add cst ctype acc) - in - let (s,acc) = - if cb.Declarations.const_body <> None - && (cb.Declarations.const_opaque || not (Cpred.mem kn knst)) - && add_opaque - then - do_type (Opaque kn) - else (s,acc) - in - match cb.Declarations.const_body with - | None -> do_type (Axiom kn) - | Some body -> aux (Declarations.force body) env s acc - - and aux_memoize_kn kn env = - try_and_go (Axiom kn) (add_kn kn env) - in - fun t env -> - snd (aux t env (ContextObjectSet.empty) (ContextObjectMap.empty)) - -(* /spiwack *) - - - diff --git a/kernel/environ.mli b/kernel/environ.mli index 7485ca37..a7795136 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: environ.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: environ.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names @@ -230,22 +230,3 @@ val unregister : env -> field -> env val register : env -> field -> Retroknowledge.entry -> env - - -(******************************************************************) -(* spiwack: a few declarations for the "Print Assumption" command *) - -type context_object = - | Variable of identifier (* A section variable or a Let definition *) - | Axiom of constant (* An axiom or a constant. *) - | Opaque of constant (* An opaque constant. *) - -(* AssumptionSet.t is a set of [assumption] *) -module OrderedContextObject : Set.OrderedType with type t = context_object -module ContextObjectMap : Map.S with type key = context_object - -(* collects all the assumptions (optionally including opaque definitions) - on which a term relies (together with their type) *) -val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t - - diff --git a/kernel/esubst.ml b/kernel/esubst.ml index 2d3956a1..82d19ec4 100644 --- a/kernel/esubst.ml +++ b/kernel/esubst.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: esubst.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: esubst.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util diff --git a/kernel/esubst.mli b/kernel/esubst.mli index 96da8dda..76c0d481 100644 --- a/kernel/esubst.mli +++ b/kernel/esubst.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: esubst.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: esubst.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s Explicit substitutions of type ['a]. *) (* - ESID(n) = %n END bounded identity diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 91aec40c..9b1ddc31 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indtypes.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: indtypes.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names @@ -247,8 +247,16 @@ let typecheck_inductive env mie = let param_ccls = List.fold_left (fun l (_,b,p) -> if b = None then let _,c = dest_prod_assum env p in - let u = match kind_of_term c with Sort (Type u) -> Some u | _ -> None in - u::l + (* Add Type levels to the ordered list of parameters contributing to *) + (* polymorphism unless there is aliasing (i.e. non distinct levels) *) + match kind_of_term c with + | Sort (Type u) -> + if List.mem (Some u) l then + None :: List.map (function Some v when u = v -> None | x -> x) l + else + Some u :: l + | _ -> + None :: l else l) [] params in diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli index 8384a63a..71d01568 100644 --- a/kernel/indtypes.mli +++ b/kernel/indtypes.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: indtypes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: indtypes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/inductive.ml b/kernel/inductive.ml index ba5e5252..62a48f07 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 13368 2010-08-03 13:22:49Z barras $ *) +(* $Id: inductive.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names @@ -186,13 +186,20 @@ let instantiate_universes env ctx ar argsorts = (* This is a Type with constraints *) else Type level -let type_of_inductive_knowing_parameters env mip paramtyps = +exception SingletonInductiveBecomesProp of identifier + +let type_of_inductive_knowing_parameters ?(polyprop=true) env mip paramtyps = match mip.mind_arity with | Monomorphic s -> s.mind_user_arity | Polymorphic ar -> let ctx = List.rev mip.mind_arity_ctxt in let ctx,s = instantiate_universes env ctx ar paramtyps in + (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e. + the situation where a non-Prop singleton inductive becomes Prop + when applied to Prop params *) + if not polyprop && not (is_type0m_univ ar.poly_level) && s = prop_sort + then raise (SingletonInductiveBecomesProp mip.mind_typename); mkArity (List.rev ctx,s) (* Type of a (non applied) inductive type *) diff --git a/kernel/inductive.mli b/kernel/inductive.mli index a2bd674f..0dac719c 100644 --- a/kernel/inductive.mli +++ b/kernel/inductive.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: inductive.mli 13368 2010-08-03 13:22:49Z barras $ i*) +(*i $Id: inductive.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names @@ -85,7 +85,16 @@ val check_cofix : env -> cofixpoint -> unit (*s Support for sort-polymorphic inductive types *) -val type_of_inductive_knowing_parameters : +(** The "polyprop" optional argument below allows to control + the "Prop-polymorphism". By default, it is allowed. + But when "polyprop=false", the following exception is raised + when a polymorphic singleton inductive type becomes Prop due to + parameter instantiation. This is used by the Ocaml extraction, + which cannot handle (yet?) Prop-polymorphism. *) + +exception SingletonInductiveBecomesProp of identifier + +val type_of_inductive_knowing_parameters : ?polyprop:bool -> env -> one_inductive_body -> types array -> types val max_inductive_sort : sorts array -> universe diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib index a628e5cf..8c1dd53a 100644 --- a/kernel/kernel.mllib +++ b/kernel/kernel.mllib @@ -29,4 +29,4 @@ Safe_typing Vm Csymtable -Vconv
\ No newline at end of file +Vconv diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml index 146da92c..ab8b60be 100644 --- a/kernel/mod_subst.ml +++ b/kernel/mod_subst.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: mod_subst.ml 13414 2010-09-14 13:28:15Z glondu $ *) +(* $Id: mod_subst.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util @@ -396,7 +396,9 @@ let subst_con sub con = let con = constant_of_delta2 resolve con' in con,mkConst con end - | Some t -> con',t + | Some t -> + (* In case of inlining, discard the canonical part (cf #2608) *) + constant_of_kn (user_con con'), t with No_subst -> con , mkConst con @@ -730,3 +732,8 @@ let subst_substituted s r = | LSlazy(s',a) -> ref (LSlazy(s::s',a)) +(* debug *) +let repr_substituted r = + match !r with + | LSval a -> None, a + | LSlazy(s,a) -> Some s, a diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli index a16ee99e..9b48b3ea 100644 --- a/kernel/mod_subst.mli +++ b/kernel/mod_subst.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_subst.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: mod_subst.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s [Mod_subst] *) @@ -135,3 +135,8 @@ val subst_mps : substitution -> constr -> constr val occur_mbid : mod_bound_id -> substitution -> bool +(** [repr_substituted r] dumps the representation of a substituted: + - [None, a] when r is a value + - [Some s, a] when r is a delayed substitution [s] applied to [a] *) + +val repr_substituted : 'a substituted -> substitution list option * 'a diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index c2a2ffee..e366bc97 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: mod_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) open Util open Names diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli index 58a80869..ec5eb332 100644 --- a/kernel/mod_typing.mli +++ b/kernel/mod_typing.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: mod_typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: mod_typing.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Declarations diff --git a/kernel/modops.ml b/kernel/modops.ml index 02662adf..f0d579a4 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.ml 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: modops.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/kernel/modops.mli b/kernel/modops.mli index 9b12fea6..37f4e8e0 100644 --- a/kernel/modops.mli +++ b/kernel/modops.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: modops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: modops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/kernel/names.ml b/kernel/names.ml index e5a9f0fc..642f5562 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: names.ml 13804 2011-01-27 00:41:34Z letouzey $ *) +(* $Id: names.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Pp open Util diff --git a/kernel/names.mli b/kernel/names.mli index f57116f9..612851dd 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: names.mli 13804 2011-01-27 00:41:34Z letouzey $ i*) +(*i $Id: names.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*s Identifiers *) diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml index bad04af5..c852ab72 100644 --- a/kernel/pre_env.ml +++ b/kernel/pre_env.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pre_env.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: pre_env.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli index 80f382c6..70776551 100644 --- a/kernel/pre_env.mli +++ b/kernel/pre_env.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: pre_env.mli 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: pre_env.mli 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 46a469df..38d1c70b 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: reduction.ml 13449 2010-09-22 19:31:50Z glondu $ *) +(* $Id: reduction.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 83a858cf..4a3e4cd5 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: reduction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: reduction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Term diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml index 799bce47..5e8dd9f8 100644 --- a/kernel/retroknowledge.ml +++ b/kernel/retroknowledge.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: retroknowledge.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: retroknowledge.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Term open Names diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli index 2a4878e9..6cf871d3 100644 --- a/kernel/retroknowledge.mli +++ b/kernel/retroknowledge.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: retroknowledge.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: retroknowledge.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index dee2f5e8..4575d5bc 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: safe_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: safe_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names @@ -40,10 +40,26 @@ type module_info = variant : modvariant; resolver : delta_resolver; resolver_of_param : delta_resolver;} - + let check_label l labset = if Labset.mem l labset then error_existing_label l +let check_labels ls senv = + Labset.iter (fun l -> check_label l senv) ls + +let labels_of_mib mib = + let add,get = + let labels = ref Labset.empty in + (fun id -> labels := Labset.add (label_of_id id) !labels), + (fun () -> !labels) + in + let visit_mip mip = + add mip.mind_typename; + Array.iter add mip.mind_consnames + in + Array.iter visit_mip mib.mind_packets; + get () + let set_engagement_opt oeng env = match oeng with Some eng -> set_engagement eng env @@ -107,22 +123,6 @@ let add_constraints cst senv = univ = Univ.Constraint.union cst senv.univ } -(*spiwack: functions for safe retroknowledge *) - -(* terms which are closed under the environnement env, i.e - terms which only depends on constant who are themselves closed *) -let closed env term = - ContextObjectMap.is_empty (assumptions full_transparent_state env term) - -(* the set of safe terms in an environement any recursive set of - terms who are known not to prove inconsistent statement. It should - include at least all the closed terms. But it could contain other ones - like the axiom of excluded middle for instance *) -let safe = - closed - - - (* universal lifting, used for the "get" operations mostly *) let retroknowledge f senv = Environ.retroknowledge f (env_of_senv senv) @@ -242,17 +242,16 @@ let add_mind dir l mie senv = if l <> label_of_id id then anomaly ("the label of inductive packet and its first inductive"^ " type do not match"); - check_label l senv.labset; - (* TODO: when we will allow reorderings we will have to verify - all labels *) let mib = translate_mind senv.env mie in + let labels = labels_of_mib mib in + check_labels labels senv.labset; let senv' = add_constraints mib.mind_constraints senv in let kn = make_mind senv.modinfo.modpath dir l in let env'' = Environ.add_mind kn mib senv'.env in kn, { old = senv'.old; env = env''; modinfo = senv'.modinfo; - labset = Labset.add l senv'.labset; (* TODO: the same as above *) + labset = Labset.union labels senv'.labset; revstruct = (l,SFBmind mib)::senv'.revstruct; univ = senv'.univ; engagement = senv'.engagement; @@ -495,12 +494,14 @@ let end_module l restype senv = (canonical_mind (mind_of_delta resolver (mind_of_kn kn))) in + let labels = labels_of_mib mib in + check_labels labels senv.labset; let senv' = add_constraints mib.mind_constraints senv in let env'' = Environ.add_mind mind mib senv'.env in { old = senv'.old; env = env''; modinfo = senv'.modinfo; - labset = Labset.add l senv'.labset; + labset = Labset.union labels senv'.labset; revstruct = (l,SFBmind mib)::senv'.revstruct; univ = senv'.univ; engagement = senv'.engagement; diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 446ee75b..33a6a775 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: safe_typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: safe_typing.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/sign.ml b/kernel/sign.ml index 0d4887ec..d241f677 100644 --- a/kernel/sign.ml +++ b/kernel/sign.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: sign.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: sign.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Names open Util diff --git a/kernel/sign.mli b/kernel/sign.mli index 313118e4..35e49003 100644 --- a/kernel/sign.mli +++ b/kernel/sign.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: sign.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: sign.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index 9216f2f3..447e062a 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.ml 13616 2010-11-03 12:14:36Z soubiran $ i*) +(*i $Id: subtyping.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Util diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli index d3736fd9..a32804b9 100644 --- a/kernel/subtyping.mli +++ b/kernel/subtyping.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: subtyping.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: subtyping.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Univ diff --git a/kernel/term.ml b/kernel/term.ml index b031f750..1894417c 100644 --- a/kernel/term.ml +++ b/kernel/term.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: term.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* This module instantiates the structure of generic deBruijn terms to Coq *) diff --git a/kernel/term.mli b/kernel/term.mli index 05a750b8..c9a97bbe 100644 --- a/kernel/term.mli +++ b/kernel/term.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term.mli 13728 2010-12-19 11:35:20Z herbelin $ i*) +(*i $Id: term.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml index 8cd9b909..c1eb97a6 100644 --- a/kernel/term_typing.ml +++ b/kernel/term_typing.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: term_typing.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: term_typing.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli index 4d32be1e..217c9f91 100644 --- a/kernel/term_typing.mli +++ b/kernel/term_typing.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: term_typing.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: term_typing.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml index 033dde90..2e6b8d50 100644 --- a/kernel/type_errors.ml +++ b/kernel/type_errors.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: type_errors.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: type_errors.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Names open Term diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli index 38ee5058..989b8fbb 100644 --- a/kernel/type_errors.mli +++ b/kernel/type_errors.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: type_errors.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: type_errors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 7527e3e7..2fd02063 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: typeops.ml 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: typeops.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Util open Names diff --git a/kernel/typeops.mli b/kernel/typeops.mli index aaacf3c5..6e922041 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: typeops.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: typeops.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (*i*) open Names diff --git a/kernel/univ.ml b/kernel/univ.ml index 9d93b16f..0646a501 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: univ.ml 13735 2010-12-21 18:21:58Z letouzey $ *) +(* $Id: univ.ml 14641 2011-11-06 11:59:10Z herbelin $ *) (* Initial Caml version originates from CoC 4.8 [Dec 1988] *) (* Extension with algebraic universes by HH [Sep 2001] *) diff --git a/kernel/univ.mli b/kernel/univ.mli index da01879c..4cb6dec1 100644 --- a/kernel/univ.mli +++ b/kernel/univ.mli @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: univ.mli 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: univ.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) (* Universes. *) diff --git a/kernel/vconv.mli b/kernel/vconv.mli index 22926d0d..e23aaf79 100644 --- a/kernel/vconv.mli +++ b/kernel/vconv.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/kernel/vm.ml b/kernel/vm.ml index ceb8ea9c..c24de162 100644 --- a/kernel/vm.ml +++ b/kernel/vm.ml @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: vm.ml 13363 2010-07-30 16:17:24Z barras $ *) +(* $Id: vm.ml 14641 2011-11-06 11:59:10Z herbelin $ *) open Names open Term |