summaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytecodes.ml2
-rw-r--r--kernel/cbytecodes.mli4
-rw-r--r--kernel/cbytegen.ml2
-rw-r--r--kernel/cemitcodes.ml2
-rw-r--r--kernel/closure.ml2
-rw-r--r--kernel/closure.mli2
-rw-r--r--kernel/conv_oracle.ml2
-rw-r--r--kernel/conv_oracle.mli2
-rw-r--r--kernel/cooking.ml8
-rw-r--r--kernel/cooking.mli5
-rw-r--r--kernel/csymtable.ml2
-rw-r--r--kernel/csymtable.mli4
-rw-r--r--kernel/declarations.ml2
-rw-r--r--kernel/declarations.mli2
-rw-r--r--kernel/entries.ml2
-rw-r--r--kernel/entries.mli2
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/esubst.ml2
-rw-r--r--kernel/esubst.mli2
-rw-r--r--kernel/indtypes.ml2
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/inductive.ml2
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/mod_subst.ml2
-rw-r--r--kernel/mod_subst.mli2
-rw-r--r--kernel/mod_typing.ml2
-rw-r--r--kernel/mod_typing.mli2
-rw-r--r--kernel/modops.ml2
-rw-r--r--kernel/modops.mli2
-rw-r--r--kernel/names.ml2
-rw-r--r--kernel/names.mli2
-rw-r--r--kernel/pre_env.ml2
-rw-r--r--kernel/pre_env.mli2
-rw-r--r--kernel/reduction.ml2
-rw-r--r--kernel/reduction.mli2
-rw-r--r--kernel/retroknowledge.ml2
-rw-r--r--kernel/retroknowledge.mli2
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/sign.ml2
-rw-r--r--kernel/sign.mli2
-rw-r--r--kernel/subtyping.ml2
-rw-r--r--kernel/subtyping.mli2
-rw-r--r--kernel/term.ml3
-rw-r--r--kernel/term.mli3
-rw-r--r--kernel/term_typing.ml5
-rw-r--r--kernel/term_typing.mli2
-rw-r--r--kernel/type_errors.ml2
-rw-r--r--kernel/type_errors.mli2
-rw-r--r--kernel/typeops.ml2
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/univ.ml2
-rw-r--r--kernel/univ.mli2
-rw-r--r--kernel/vconv.mli2
-rw-r--r--kernel/vm.ml2
56 files changed, 69 insertions, 61 deletions
diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 8854f854..c0119aa2 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index c5d483ac..da34d81e 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cbytecodes.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: cbytecodes.mli 15714 2012-08-08 18:54:37Z herbelin $ *)
open Names
open Term
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 8da06f43..fb749e31 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml
index 1f00a70e..00f1f7fb 100644
--- a/kernel/cemitcodes.ml
+++ b/kernel/cemitcodes.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 143d6eb4..d4f3efd5 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index f4dc5db3..26adc226 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml
index 92109258..2879391b 100644
--- a/kernel/conv_oracle.ml
+++ b/kernel/conv_oracle.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli
index 09ca4b92..f875fabf 100644
--- a/kernel/conv_oracle.mli
+++ b/kernel/conv_oracle.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 02330339..ae717353 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -135,6 +135,10 @@ let cook_constant env r =
(fun c -> abstract_constant_body (expmod_constr r.d_modlist c) hyps)
cb.const_body
in
+ let const_hyps =
+ Sign.fold_named_context (fun (h,_,_) hyps ->
+ List.filter (fun (id,_,_) -> id <> h) hyps)
+ hyps ~init:cb.const_hyps in
let typ = match cb.const_type with
| NonPolymorphicType t ->
let typ = abstract_constant_type (expmod_constr r.d_modlist t) hyps in
@@ -145,4 +149,4 @@ let cook_constant env r =
let j = make_judge (constr_of_def body) typ in
Typeops.make_polymorphic_if_constant_for_ind env j
in
- (body, typ, cb.const_constraints)
+ (body, typ, cb.const_constraints, const_hyps)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 5f31ff8c..1586adae 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -22,7 +22,8 @@ type recipe = {
d_modlist : work_list }
val cook_constant :
- env -> recipe -> constant_def * constant_type * constraints
+ env -> recipe ->
+ constant_def * constant_type * constraints * Sign.section_context
(** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index e8b66d09..8d09cbd7 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/csymtable.mli b/kernel/csymtable.mli
index 8c1ad98b..565c31ae 100644
--- a/kernel/csymtable.mli
+++ b/kernel/csymtable.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: csymtable.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: csymtable.mli 15714 2012-08-08 18:54:37Z herbelin $ *)
open Names
open Term
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1a84b987..5f677d05 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 7cf74ba3..a298d56a 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/entries.ml b/kernel/entries.ml
index a4485fac..f17918a6 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index b726d0ec..2460ec64 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 7a41e62c..39ada672 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 42100e4e..7b1c1d41 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/esubst.ml b/kernel/esubst.ml
index cbce04d6..0bd7c515 100644
--- a/kernel/esubst.ml
+++ b/kernel/esubst.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/esubst.mli b/kernel/esubst.mli
index fe978261..8cc3a1d0 100644
--- a/kernel/esubst.mli
+++ b/kernel/esubst.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 46e866a0..0dd2cd69 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index b37aefe4..4d71a81d 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 21f86233..53a1525b 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index a124647c..89ba7869 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 314cc0ee..15a48e1c 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 55d2ff15..21b6bf93 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index bfc6f3c7..3a4c93ec 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 0987ca5b..0990e36c 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0c2c6bd7..af32288c 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/modops.mli b/kernel/modops.mli
index b9c36d5a..d03d61bd 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/names.ml b/kernel/names.ml
index ae8ad093..17bda124 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/names.mli b/kernel/names.mli
index 34c5e62c..24b16f28 100644
--- a/kernel/names.mli
+++ b/kernel/names.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 985aac95..6c08c34c 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index 40ce887b..7d32b8fa 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index fc5e32cf..6c52e151 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index aa78fbda..acc97380 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/retroknowledge.ml b/kernel/retroknowledge.ml
index 10d0bae7..6f52edcd 100644
--- a/kernel/retroknowledge.ml
+++ b/kernel/retroknowledge.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/retroknowledge.mli b/kernel/retroknowledge.mli
index b9793f6d..88bdf706 100644
--- a/kernel/retroknowledge.mli
+++ b/kernel/retroknowledge.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index d7a8b005..1d606782 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index ad275d49..34dc68d2 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 71169563..a654bc04 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 074139c9..4325fe90 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 08ee67b4..e2c5f48c 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/subtyping.mli b/kernel/subtyping.mli
index cf9cb540..d3a48a8a 100644
--- a/kernel/subtyping.mli
+++ b/kernel/subtyping.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/term.ml b/kernel/term.ml
index 46bc7c56..2b4547d0 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -264,6 +264,7 @@ let destMeta c = match kind_of_term c with
| _ -> invalid_arg "destMeta"
let isMeta c = match kind_of_term c with Meta _ -> true | _ -> false
+let isMetaOf mv c = match kind_of_term c with Meta mv' -> mv = mv' | _ -> false
(* Destructs a variable *)
let destVar c = match kind_of_term c with
diff --git a/kernel/term.mli b/kernel/term.mli
index e83be6d6..15fcdd18 100644
--- a/kernel/term.mli
+++ b/kernel/term.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -235,6 +235,7 @@ val isVarId : identifier -> constr -> bool
val isInd : constr -> bool
val isEvar : constr -> bool
val isMeta : constr -> bool
+val isMetaOf : metavariable -> constr -> bool
val isEvar_or_Meta : constr -> bool
val isSort : constr -> bool
val isCast : constr -> bool
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 478b9c6f..ee5e8fda 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -150,7 +150,8 @@ let translate_constant env kn ce =
let translate_recipe env kn r =
build_constant_declaration env kn
- (let def,typ,cst = Cooking.cook_constant env r in def,typ,cst,None)
+ (let def,typ,cst,hyps = Cooking.cook_constant env r in
+ def,typ,cst,Some hyps)
(* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index 3bbf5667..c2f046a2 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index 8f129999..890f0976 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 7c61e105..1967018f 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 49106c91..affd4dc4 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index c1c805f3..51f36d6d 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 0193542a..6aeb7390 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index e4e66915..22723713 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 2d65170c..4168e501 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-2012 *)
(* \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 86aed5d9..ebf1e8fd 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -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-2012 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)