summaryrefslogtreecommitdiff
path: root/toplevel
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/auto_ind_decl.ml4
-rw-r--r--toplevel/auto_ind_decl.mli2
-rw-r--r--toplevel/autoinstance.ml4
-rw-r--r--toplevel/autoinstance.mli2
-rw-r--r--toplevel/cerrors.ml4
-rw-r--r--toplevel/cerrors.mli4
-rw-r--r--toplevel/class.ml4
-rw-r--r--toplevel/class.mli4
-rw-r--r--toplevel/classes.ml8
-rw-r--r--toplevel/classes.mli4
-rw-r--r--toplevel/command.ml4
-rw-r--r--toplevel/command.mli4
-rw-r--r--toplevel/coqinit.ml4
-rw-r--r--toplevel/coqinit.mli4
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/coqtop.mli4
-rw-r--r--toplevel/discharge.ml13
-rw-r--r--toplevel/discharge.mli4
-rw-r--r--toplevel/himsg.ml4
-rw-r--r--toplevel/himsg.mli4
-rw-r--r--toplevel/ind_tables.ml4
-rw-r--r--toplevel/ind_tables.mli2
-rw-r--r--toplevel/indschemes.ml26
-rw-r--r--toplevel/indschemes.mli4
-rw-r--r--toplevel/lemmas.ml4
-rw-r--r--toplevel/lemmas.mli4
-rw-r--r--toplevel/libtypes.ml2
-rw-r--r--toplevel/libtypes.mli2
-rw-r--r--toplevel/metasyntax.ml4
-rw-r--r--toplevel/metasyntax.mli4
-rw-r--r--toplevel/mltop.ml44
-rw-r--r--toplevel/mltop.mli4
-rw-r--r--toplevel/record.ml9
-rw-r--r--toplevel/record.mli4
-rw-r--r--toplevel/search.ml4
-rw-r--r--toplevel/search.mli4
-rw-r--r--toplevel/toplevel.ml4
-rw-r--r--toplevel/toplevel.mli4
-rw-r--r--toplevel/usage.ml4
-rw-r--r--toplevel/usage.mli4
-rw-r--r--toplevel/vernac.ml4
-rw-r--r--toplevel/vernac.mli4
-rw-r--r--toplevel/vernacentries.ml15
-rw-r--r--toplevel/vernacentries.mli4
-rw-r--r--toplevel/vernacexpr.ml4
-rw-r--r--toplevel/vernacinterp.ml4
-rw-r--r--toplevel/vernacinterp.mli4
-rw-r--r--toplevel/whelp.ml44
-rw-r--r--toplevel/whelp.mli4
49 files changed, 122 insertions, 115 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 6064c3d4..16ceffed 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.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: auto_ind_decl.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: auto_ind_decl.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* This file is about the automatic generation of schemes about
decidable equality, created by Vincent Siles, Oct 2007 *)
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index fc7aecad..c791da28 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.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/toplevel/autoinstance.ml b/toplevel/autoinstance.ml
index 62a97281..4a67ede4 100644
--- a/toplevel/autoinstance.ml
+++ b/toplevel/autoinstance.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-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -191,7 +191,7 @@ let declare_class_instance gr ctx params =
let ident = make_instance_ident gr in
let cl = Typeclasses.class_info gr in
let (def,typ) = Typeclasses.instance_constructor cl params in
- let (def,typ) = it_mkLambda_or_LetIn def ctx, it_mkProd_or_LetIn typ ctx in
+ let (def,typ) = it_mkLambda_or_LetIn (Option.get def) ctx, it_mkProd_or_LetIn typ ctx in
let def = deep_refresh_universes def in
let typ = deep_refresh_universes typ in
let ce = Entries.DefinitionEntry
diff --git a/toplevel/autoinstance.mli b/toplevel/autoinstance.mli
index 9478aa16..b9b1e3c2 100644
--- a/toplevel/autoinstance.mli
+++ b/toplevel/autoinstance.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/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 3bba0605..86057b4b 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.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: cerrors.ml 13639 2010-11-16 15:36:01Z glondu $ *)
+(* $Id: cerrors.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 31e0e04f..e1f7c035 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.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: cerrors.mli 13431 2010-09-18 08:15:29Z herbelin $ i*)
+(*i $Id: cerrors.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 0ee9dd19..09ce84e0 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.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: class.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: class.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Pp
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 057d85ac..b05f38e7 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.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: class.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: class.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2d8aabfc..28c1ab75 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -1,13 +1,13 @@
(* -*- compile-command: "make -C .. bin/coqtop.byte" -*- *)
(************************************************************************)
(* 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: classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*)
+(*i $Id: classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
@@ -245,8 +245,8 @@ let new_instance ?(abstract=false) ?(global=false) ctx (instid, bk, cl) props
in
let app, ty_constr = instance_constructor k subst in
let termtype = it_mkProd_or_LetIn ty_constr (ctx' @ ctx) in
- let term = Termops.it_mkLambda_or_LetIn app (ctx' @ ctx) in
- term, termtype
+ let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
+ term, termtype
| Inr (def, subst) ->
let termtype = it_mkProd_or_LetIn cty ctx in
let term = Termops.it_mkLambda_or_LetIn def ctx in
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 61670e0d..69e4dd8b 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.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: classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 2d0cdea6..1112ac6d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.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: command.ml 13672 2010-12-03 20:05:46Z herbelin $ *)
+(* $Id: command.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/command.mli b/toplevel/command.mli
index f5996905..af89b59a 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.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: command.mli 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: command.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Util
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index bce38128..210507e1 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.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: coqinit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coqinit.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open System
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index c2a535dd..c0f59a56 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.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: coqinit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coqinit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* Initialization. *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index f05509a4..7887a060 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.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: coqtop.ml 13358 2010-07-29 23:10:17Z herbelin $ *)
+(* $Id: coqtop.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index e80b3252..ef730915 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.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: coqtop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: coqtop.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* The Coq main module. The following function [start] will parse the
command line, print the banner, initialize the load path, load the input
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 6f74c526..58122e11 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.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: discharge.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: discharge.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Names
open Util
@@ -67,13 +67,20 @@ let abstract_inductive hyps nparams inds =
inds'
in (params',ind'')
+let refresh_polymorphic_type_of_inductive (_,mip) =
+ match mip.mind_arity with
+ | Monomorphic s ->
+ s.mind_user_arity
+ | Polymorphic ar ->
+ let ctx = List.rev mip.mind_arity_ctxt in
+ mkArity (List.rev ctx,Termops.new_Type_sort())
let process_inductive sechyps modlist mib =
let nparams = mib.mind_nparams in
let inds =
array_map_to_list
(fun mip ->
- let arity = expmod_constr modlist (Termops.refresh_universes_strict (Inductive.type_of_inductive (Global.env()) (mib,mip))) in
+ let arity = expmod_constr modlist (refresh_polymorphic_type_of_inductive (mib,mip)) in
let lc = Array.map (expmod_constr modlist) mip.mind_user_lc in
(mip.mind_typename,
arity,
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index dda4c5d7..f881e8a2 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.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: discharge.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: discharge.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Sign
open Cooking
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 99ca9879..62d19bea 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.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: himsg.ml 13465 2010-09-24 22:23:07Z herbelin $ *)
+(* $Id: himsg.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index a916e87b..e12e445c 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.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: himsg.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: himsg.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index c2d5f31d..53c3bcea 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.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: ind_tables.ml 13392 2010-09-02 12:11:15Z vsiles $ i*)
+(*i $Id: ind_tables.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* File created by Vincent Siles, Oct 2007, extended into a generic
support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *)
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index 1374a0a4..e6f5e77a 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.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/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 9031d8a3..3596085f 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.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: indschemes.ml 13396 2010-09-02 16:52:15Z vsiles $ *)
+(* $Id: indschemes.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* Created by Hugo Herbelin from contents related to inductive schemes
initially developed by Christine Paulin (induction schemes), Vincent
@@ -295,34 +295,34 @@ requested
*)
| (None,t)::q ->
let l1,l2 = split_scheme q in
- let names inds recs x y z =
+ let names inds recs isdep y z =
let ind = smart_global_inductive y in
- let sort_of_ind = Retyping.get_sort_family_of env Evd.empty (mkInd ind) in
+ let sort_of_ind = inductive_sort_family (snd (lookup_mind_specif env ind)) in
let z' = family_of_sort (interp_sort z) in
let suffix = (
match sort_of_ind with
| InProp ->
- if x then (match z' with
- | InProp -> inds ^ "_nodep"
- | InSet -> recs ^ "_nodep"
- | InType -> recs ^ "t_nodep")
+ if isdep then (match z' with
+ | InProp -> inds ^ "_dep"
+ | InSet -> recs ^ "_dep"
+ | InType -> recs ^ "t_dep")
else ( match z' with
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
| _ ->
- if x then (match z' with
+ if isdep then (match z' with
| InProp -> inds
| InSet -> recs
| InType -> recs ^ "t" )
else (match z' with
- | InProp -> inds ^ "_dep"
- | InSet -> recs ^ "_dep"
- | InType -> recs ^ "t_dep")
+ | InProp -> inds ^ "_nodep"
+ | InSet -> recs ^ "_nodep"
+ | InType -> recs ^ "t_nodep")
) in
let newid = add_suffix (basename_of_global (IndRef ind)) suffix in
let newref = (dummy_loc,newid) in
- ((newref,x,ind,z)::l1),l2
+ ((newref,isdep,ind,z)::l1),l2
in
match t with
| CaseScheme (x,y,z) -> names "_case" "_case" x y z
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index f763e182..707b9e00 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.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: indschemes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: indschemes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Util
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 7af5d0aa..8ef82105 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.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: lemmas.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: lemmas.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* Created by Hugo Herbelin from contents related to lemma proofs in
file command.ml, Aug 2009 *)
diff --git a/toplevel/lemmas.mli b/toplevel/lemmas.mli
index 5327f63f..0e8eaac2 100644
--- a/toplevel/lemmas.mli
+++ b/toplevel/lemmas.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: lemmas.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: lemmas.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/libtypes.ml b/toplevel/libtypes.ml
index 41680036..27e19bd8 100644
--- a/toplevel/libtypes.ml
+++ b/toplevel/libtypes.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-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/libtypes.mli b/toplevel/libtypes.mli
index f3839ec1..03329592 100644
--- a/toplevel/libtypes.mli
+++ b/toplevel/libtypes.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/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index c1663685..0adae08a 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.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: metasyntax.ml 13690 2010-12-06 16:15:54Z glondu $ *)
+(* $Id: metasyntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Flags
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index d8dd0d52..2c4e29bb 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.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: metasyntax.mli 13328 2010-07-26 11:05:30Z herbelin $ i*)
+(*i $Id: metasyntax.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Util
diff --git a/toplevel/mltop.ml4 b/toplevel/mltop.ml4
index e8c06d13..59bc01d0 100644
--- a/toplevel/mltop.ml4
+++ b/toplevel/mltop.ml4
@@ -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 *)
@@ -11,7 +11,7 @@
* camlp4deps will not work for this file unless Makefile system enhanced.
*)
-(* $Id: mltop.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: mltop.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Pp
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 12b6f78f..ae562bd2 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.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: mltop.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: mltop.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* If there is a toplevel under Coq, it is described by the following
record. *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 773d3390..ee9b8d66 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.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: record.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: record.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
@@ -137,7 +137,10 @@ let subst_projection fid l c =
match List.nth l (k-depth-2) with
| Projection t -> lift depth t
| NoProjection (Name id) -> bad_projs := id :: !bad_projs; mkRel k
- | NoProjection Anonymous -> assert false
+ | NoProjection Anonymous ->
+ errorlabstrm "" (str "Field " ++ pr_id fid ++
+ str " depends on the " ++ str (ordinal (k-depth-1)) ++ str
+ " field which has no name.")
else
mkRel (k-lv)
| _ -> map_constr_with_binders succ substrec depth c
diff --git a/toplevel/record.mli b/toplevel/record.mli
index ea4a3b7e..44b34550 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.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: record.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: record.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 574983cd..fd3024a4 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.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: search.ml 13853 2011-02-24 07:57:31Z glondu $ *)
+(* $Id: search.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/search.mli b/toplevel/search.mli
index a73052f2..6a85a12f 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.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: search.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: search.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Pp
open Names
diff --git a/toplevel/toplevel.ml b/toplevel/toplevel.ml
index 299214f0..9954ff56 100644
--- a/toplevel/toplevel.ml
+++ b/toplevel/toplevel.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: toplevel.ml 13668 2010-12-02 17:43:59Z herbelin $ *)
+(* $Id: toplevel.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index a614c1da..022a6541 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.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: toplevel.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: toplevel.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Pp
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 22588f2c..0282f30a 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.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: usage.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: usage.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
let version () =
Printf.printf "The Coq Proof Assistant, version %s (%s)\n"
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 1167750b..721edccb 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.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: usage.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: usage.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*s Prints the version number on the standard output and exits (with 0). *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index afc5057e..a7aef93f 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.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: vernac.ml 13923 2011-03-21 16:25:20Z letouzey $ *)
+(* $Id: vernac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* Parsing of vernacular. *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index dc4d9e2f..54ce9244 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.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: vernac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: vernac.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* Parsing of vernacular. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 7710cb95..3be3c6db 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.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: vernacentries.ml 13922 2011-03-21 16:25:18Z letouzey $ i*)
+(*i $Id: vernacentries.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -370,9 +370,6 @@ let vernac_exact_proof c =
(strbrk "Command 'Proof ...' can only be used at the beginning of the proof.")
let vernac_assumption kind l nl=
- if Pfedit.refining () then
- errorlabstrm ""
- (str "Cannot declare an assumption while in proof editing mode.");
let global = fst kind = Global in
List.iter (fun (is_coe,(idl,c)) ->
if Dumpglob.dump () then
@@ -1113,12 +1110,12 @@ let vernac_print = function
pp (Notation.pr_visibility (Constrextern.without_symbols pr_lrawconstr) s)
| PrintAbout qid -> msg (print_about qid)
| PrintImplicit qid -> msg (print_impargs qid)
-(*spiwack: prints all the axioms and section variables used by a term *)
| PrintAssumptions (o,r) ->
+ (* Prints all the axioms and section variables used by a term *)
let cstr = constr_of_global (smart_global r) in
- let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
- ~add_opaque:o cstr (Global.env ()) in
- msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
+ let st = Conv_oracle.get_transp_state () in
+ let nassums = Assumptions.assumptions st ~add_opaque:o cstr in
+ msg (Printer.pr_assumptionset (Global.env ()) nassums)
let global_module r =
let (loc,qid) = qualid_of_reference r in
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 10ed35a7..1cca3540 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.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: vernacentries.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: vernacentries.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 0d247189..31c46a54 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.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: vernacexpr.ml 13668 2010-12-02 17:43:59Z herbelin $ i*)
+(*i $Id: vernacexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Util
open Names
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index f3d2e7a5..e6fe9a4f 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.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: vernacinterp.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: vernacinterp.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index ce64188c..780e4e28 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.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: vernacinterp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: vernacinterp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Tacexpr
diff --git a/toplevel/whelp.ml4 b/toplevel/whelp.ml4
index 15caaddd..e380ae6f 100644
--- a/toplevel/whelp.ml4
+++ b/toplevel/whelp.ml4
@@ -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 *)
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: whelp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: whelp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Flags
open Pp
diff --git a/toplevel/whelp.mli b/toplevel/whelp.mli
index 27c36239..75e9ad49 100644
--- a/toplevel/whelp.mli
+++ b/toplevel/whelp.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: whelp.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: whelp.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* Coq interface to the Whelp query engine developed at
the University of Bologna *)