Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

20 files changed, 21 insertions, 19 deletions

diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index c9556972..882bcae9 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -8,6 +8,8 @@
 
 (** Extraction to Ocaml : use of basic Ocaml types *)
 
+Scheme Equality for nat.
+
 Extract Inductive bool => bool [ true false ].
 Extract Inductive option => option [ Some None ].
 Extract Inductive unit => unit [ "()" ].
diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 72429055..ca72f873 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: common.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Pp
 open Util
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index 0d2258a8..619cddfb 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: common.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Libnames
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 36df8d16..58d8fcb1 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extract_env.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Term
 open Declarations
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index 7520e6c8..b4516898 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extract_env.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s This module declares the extraction commands. *)
 
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index f031094a..057057d1 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extraction.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 394e5ab7..0574b009 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: extraction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Extraction from Coq terms to Miniml. *)
 
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index dd1e7149..57b7c365 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: haskell.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Production of Haskell syntax. *)
 
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 915b8a95..0b68e73b 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: haskell.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 val haskell_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index d768ec96..7ff11b90 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: miniml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Target language for extraction: a core ML called MiniML. *)
 
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 2c63e588..745a78fe 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: mlutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Pp
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index a692e6d5..d6b85f12 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: mlutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Util
 open Names
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 8369ba91..15145344 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: modutil.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Declarations
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index 5a159dc7..bb405d60 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: modutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Declarations
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index ae8ec249..36ca3713 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: ocaml.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Production of Ocaml syntax. *)
 
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 646b1c8b..477b4351 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: ocaml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 val ocaml_descr : Miniml.language_descr
 
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 82fac0b6..fa293ba1 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: scheme.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*s Production of Scheme syntax. *)
 
diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli
index 7bb97cf9..e413d31e 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -6,6 +6,6 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: scheme.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 val scheme_descr : Miniml.language_descr
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index e33e1e06..fd640388 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: table.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 96592f19..a3199b50 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: table.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Libnames