From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- plugins/extraction/ExtrOcamlBasic.v | 2 ++ plugins/extraction/common.ml | 2 +- plugins/extraction/common.mli | 2 +- plugins/extraction/extract_env.ml | 2 +- plugins/extraction/extract_env.mli | 2 +- plugins/extraction/extraction.ml | 2 +- plugins/extraction/extraction.mli | 2 +- plugins/extraction/haskell.ml | 2 +- plugins/extraction/haskell.mli | 2 +- plugins/extraction/miniml.mli | 2 +- plugins/extraction/mlutil.ml | 2 +- plugins/extraction/mlutil.mli | 2 +- plugins/extraction/modutil.ml | 2 +- plugins/extraction/modutil.mli | 2 +- plugins/extraction/ocaml.ml | 2 +- plugins/extraction/ocaml.mli | 2 +- plugins/extraction/scheme.ml | 2 +- plugins/extraction/scheme.mli | 2 +- plugins/extraction/table.ml | 2 +- plugins/extraction/table.mli | 2 +- 20 files changed, 21 insertions(+), 19 deletions(-) (limited to 'plugins/extraction') 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 -- cgit v1.2.3