summaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml4
-rw-r--r--plugins/cc/ccalgo.mli4
-rw-r--r--plugins/cc/ccproof.ml4
-rw-r--r--plugins/cc/ccproof.mli4
-rw-r--r--plugins/cc/cctac.ml4
-rw-r--r--plugins/cc/cctac.mli4
-rw-r--r--plugins/cc/g_congruence.ml44
-rw-r--r--plugins/dp/g_dp.ml44
-rw-r--r--plugins/extraction/ExtrOcamlBasic.v2
-rw-r--r--plugins/extraction/ExtrOcamlBigIntConv.v2
-rw-r--r--plugins/extraction/ExtrOcamlIntConv.v2
-rw-r--r--plugins/extraction/ExtrOcamlNatBigInt.v2
-rw-r--r--plugins/extraction/ExtrOcamlNatInt.v2
-rw-r--r--plugins/extraction/ExtrOcamlString.v2
-rw-r--r--plugins/extraction/ExtrOcamlZBigInt.v2
-rw-r--r--plugins/extraction/ExtrOcamlZInt.v2
-rw-r--r--plugins/extraction/big.ml2
-rw-r--r--plugins/extraction/common.ml22
-rw-r--r--plugins/extraction/common.mli4
-rw-r--r--plugins/extraction/extract_env.ml22
-rw-r--r--plugins/extraction/extract_env.mli4
-rw-r--r--plugins/extraction/extraction.ml47
-rw-r--r--plugins/extraction/extraction.mli4
-rw-r--r--plugins/extraction/g_extraction.ml42
-rw-r--r--plugins/extraction/haskell.ml8
-rw-r--r--plugins/extraction/haskell.mli4
-rw-r--r--plugins/extraction/miniml.mli6
-rw-r--r--plugins/extraction/mlutil.ml57
-rw-r--r--plugins/extraction/mlutil.mli6
-rw-r--r--plugins/extraction/modutil.ml6
-rw-r--r--plugins/extraction/modutil.mli4
-rw-r--r--plugins/extraction/ocaml.ml94
-rw-r--r--plugins/extraction/ocaml.mli4
-rw-r--r--plugins/extraction/scheme.ml4
-rw-r--r--plugins/extraction/scheme.mli4
-rw-r--r--plugins/extraction/table.ml34
-rw-r--r--plugins/extraction/table.mli6
-rw-r--r--plugins/field/LegacyField.v4
-rw-r--r--plugins/field/LegacyField_Compl.v4
-rw-r--r--plugins/field/LegacyField_Tactic.v4
-rw-r--r--plugins/field/LegacyField_Theory.v4
-rw-r--r--plugins/field/field.ml44
-rw-r--r--plugins/firstorder/formula.ml4
-rw-r--r--plugins/firstorder/formula.mli4
-rw-r--r--plugins/firstorder/g_ground.ml44
-rw-r--r--plugins/firstorder/ground.ml4
-rw-r--r--plugins/firstorder/ground.mli4
-rw-r--r--plugins/firstorder/instances.ml4
-rw-r--r--plugins/firstorder/instances.mli4
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/firstorder/sequent.mli4
-rw-r--r--plugins/firstorder/unify.ml4
-rw-r--r--plugins/firstorder/unify.mli4
-rw-r--r--plugins/fourier/Fourier.v4
-rw-r--r--plugins/fourier/Fourier_util.v4
-rw-r--r--plugins/fourier/fourier.ml4
-rw-r--r--plugins/fourier/fourierR.ml4
-rw-r--r--plugins/fourier/g_fourier.ml44
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/invfun.ml11
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/rawterm_to_relation.ml79
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/micromega/CheckerMaker.v2
-rw-r--r--plugins/micromega/Env.v2
-rw-r--r--plugins/micromega/EnvRing.v2
-rw-r--r--plugins/micromega/MExtraction.v2
-rw-r--r--plugins/micromega/OrderedRing.v2
-rw-r--r--plugins/micromega/Psatz.v2
-rw-r--r--plugins/micromega/QMicromega.v2
-rw-r--r--plugins/micromega/RMicromega.v2
-rw-r--r--plugins/micromega/Refl.v2
-rw-r--r--plugins/micromega/RingMicromega.v2
-rw-r--r--plugins/micromega/Tauto.v2
-rw-r--r--plugins/micromega/VarMap.v2
-rw-r--r--plugins/micromega/ZCoeff.v2
-rw-r--r--plugins/micromega/ZMicromega.v2
-rw-r--r--plugins/micromega/certificate.ml2
-rw-r--r--plugins/micromega/coq_micromega.ml2
-rw-r--r--plugins/micromega/csdpcert.ml2
-rw-r--r--plugins/micromega/g_micromega.ml44
-rw-r--r--plugins/micromega/mutils.ml2
-rw-r--r--plugins/micromega/persistent_cache.ml2
-rw-r--r--plugins/micromega/sos.mli2
-rw-r--r--plugins/micromega/sos_types.ml2
-rw-r--r--plugins/nsatz/Nsatz.v2
-rw-r--r--plugins/nsatz/ideal.ml2
-rw-r--r--plugins/nsatz/nsatz.ml42
-rw-r--r--plugins/nsatz/polynom.ml2
-rw-r--r--plugins/nsatz/polynom.mli2
-rw-r--r--plugins/omega/Omega.v4
-rw-r--r--plugins/omega/OmegaPlugin.v4
-rw-r--r--plugins/omega/coq_omega.ml4
-rw-r--r--plugins/omega/g_omega.ml44
-rw-r--r--plugins/omega/omega.ml2
-rw-r--r--plugins/quote/Quote.v4
-rw-r--r--plugins/quote/g_quote.ml44
-rw-r--r--plugins/quote/quote.ml4
-rw-r--r--plugins/ring/LegacyArithRing.v4
-rw-r--r--plugins/ring/LegacyNArithRing.v4
-rw-r--r--plugins/ring/LegacyRing.v4
-rw-r--r--plugins/ring/LegacyRing_theory.v4
-rw-r--r--plugins/ring/LegacyZArithRing.v4
-rw-r--r--plugins/ring/Ring_abstract.v4
-rw-r--r--plugins/ring/Ring_normalize.v4
-rw-r--r--plugins/ring/Setoid_ring.v4
-rw-r--r--plugins/ring/Setoid_ring_normalize.v4
-rw-r--r--plugins/ring/Setoid_ring_theory.v4
-rw-r--r--plugins/ring/g_ring.ml44
-rw-r--r--plugins/ring/ring.ml4
-rw-r--r--plugins/rtauto/Bintree.v4
-rw-r--r--plugins/rtauto/Rtauto.v4
-rw-r--r--plugins/rtauto/g_rtauto.ml44
-rw-r--r--plugins/rtauto/proof_search.ml4
-rw-r--r--plugins/rtauto/proof_search.mli4
-rw-r--r--plugins/rtauto/refl_tauto.ml4
-rw-r--r--plugins/rtauto/refl_tauto.mli4
-rw-r--r--plugins/setoid_ring/ArithRing.v2
-rw-r--r--plugins/setoid_ring/BinList.v2
-rw-r--r--plugins/setoid_ring/Field.v2
-rw-r--r--plugins/setoid_ring/Field_tac.v2
-rw-r--r--plugins/setoid_ring/Field_theory.v2
-rw-r--r--plugins/setoid_ring/InitialRing.v2
-rw-r--r--plugins/setoid_ring/NArithRing.v2
-rw-r--r--plugins/setoid_ring/Ring.v2
-rw-r--r--plugins/setoid_ring/Ring_base.v2
-rw-r--r--plugins/setoid_ring/Ring_polynom.v2
-rw-r--r--plugins/setoid_ring/Ring_theory.v2
-rw-r--r--plugins/setoid_ring/ZArithRing.v2
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--plugins/subtac/eterm.mli4
-rw-r--r--plugins/subtac/g_subtac.ml44
-rw-r--r--plugins/subtac/subtac.ml4
-rw-r--r--plugins/subtac/subtac_cases.ml4
-rw-r--r--plugins/subtac/subtac_cases.mli4
-rw-r--r--plugins/subtac/subtac_classes.ml6
-rw-r--r--plugins/subtac/subtac_classes.mli4
-rw-r--r--plugins/subtac/subtac_coercion.ml4
-rw-r--r--plugins/subtac/subtac_pretyping.ml4
-rw-r--r--plugins/subtac/subtac_pretyping_F.ml4
-rw-r--r--plugins/subtac/subtac_utils.ml6
-rw-r--r--plugins/syntax/nat_syntax.ml4
-rw-r--r--plugins/syntax/numbers_syntax.ml4
-rw-r--r--plugins/syntax/r_syntax.ml4
-rw-r--r--plugins/syntax/z_syntax.ml4
-rw-r--r--plugins/xml/acic.ml2
-rw-r--r--plugins/xml/acic2Xml.ml42
-rw-r--r--plugins/xml/cic2acic.ml2
-rw-r--r--plugins/xml/doubleTypeInference.ml2
-rw-r--r--plugins/xml/doubleTypeInference.mli2
-rw-r--r--plugins/xml/dumptree.ml42
-rw-r--r--plugins/xml/proof2aproof.ml2
-rw-r--r--plugins/xml/proofTree2Xml.ml42
-rw-r--r--plugins/xml/unshare.ml2
-rw-r--r--plugins/xml/unshare.mli2
-rw-r--r--plugins/xml/xml.ml42
-rw-r--r--plugins/xml/xml.mli4
-rw-r--r--plugins/xml/xmlcommand.ml2
-rw-r--r--plugins/xml/xmlcommand.mli4
-rw-r--r--plugins/xml/xmlentries.ml44
163 files changed, 515 insertions, 359 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 82b4143e..3c40cfb9 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.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: ccalgo.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
+(* $Id: ccalgo.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* This file implements the basic congruence-closure algorithm by *)
(* Downey,Sethi and Tarjan. *)
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index 2825be1a..8786c907 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccalgo.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccalgo.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Term
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index 5ee17b6e..6981c5a0 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.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: ccproof.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccproof.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* This file uses the (non-compressed) union-find structure to generate *)
(* proof-trees that will be transformed into proof-terms in cctac.ml4 *)
diff --git a/plugins/cc/ccproof.mli b/plugins/cc/ccproof.mli
index 4c75f9b0..a58637f9 100644
--- a/plugins/cc/ccproof.mli
+++ b/plugins/cc/ccproof.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ccproof.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ccproof.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Ccalgo
open Names
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index ca1a9085..5b477b4d 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.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 *)
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: cctac.ml 13409 2010-09-13 07:53:13Z soubiran $ *)
+(* $Id: cctac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* This file is the interface between the c-c algorithm and Coq *)
diff --git a/plugins/cc/cctac.mli b/plugins/cc/cctac.mli
index 1c07cabf..b3d5c16b 100644
--- a/plugins/cc/cctac.mli
+++ b/plugins/cc/cctac.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: cctac.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: cctac.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Proof_type
diff --git a/plugins/cc/g_congruence.ml4 b/plugins/cc/g_congruence.ml4
index bed77a7b..eb58c5eb 100644
--- a/plugins/cc/g_congruence.ml4
+++ b/plugins/cc/g_congruence.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: g_congruence.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_congruence.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Cctac
open Tactics
diff --git a/plugins/dp/g_dp.ml4 b/plugins/dp/g_dp.ml4
index 9c61aad5..fc957ea6 100644
--- a/plugins/dp/g_dp.ml4
+++ b/plugins/dp/g_dp.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: g_dp.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_dp.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Dp
diff --git a/plugins/extraction/ExtrOcamlBasic.v b/plugins/extraction/ExtrOcamlBasic.v
index 882bcae9..eab2f67c 100644
--- a/plugins/extraction/ExtrOcamlBasic.v
+++ b/plugins/extraction/ExtrOcamlBasic.v
@@ -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/plugins/extraction/ExtrOcamlBigIntConv.v b/plugins/extraction/ExtrOcamlBigIntConv.v
index 69e72918..e38d41e3 100644
--- a/plugins/extraction/ExtrOcamlBigIntConv.v
+++ b/plugins/extraction/ExtrOcamlBigIntConv.v
@@ -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/plugins/extraction/ExtrOcamlIntConv.v b/plugins/extraction/ExtrOcamlIntConv.v
index 697ea6b3..b059b2a0 100644
--- a/plugins/extraction/ExtrOcamlIntConv.v
+++ b/plugins/extraction/ExtrOcamlIntConv.v
@@ -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/plugins/extraction/ExtrOcamlNatBigInt.v b/plugins/extraction/ExtrOcamlNatBigInt.v
index 61dc7313..1fb83c5b 100644
--- a/plugins/extraction/ExtrOcamlNatBigInt.v
+++ b/plugins/extraction/ExtrOcamlNatBigInt.v
@@ -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/plugins/extraction/ExtrOcamlNatInt.v b/plugins/extraction/ExtrOcamlNatInt.v
index da0af5cc..e577ebe1 100644
--- a/plugins/extraction/ExtrOcamlNatInt.v
+++ b/plugins/extraction/ExtrOcamlNatInt.v
@@ -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/plugins/extraction/ExtrOcamlString.v b/plugins/extraction/ExtrOcamlString.v
index f8f942c8..48260e3d 100644
--- a/plugins/extraction/ExtrOcamlString.v
+++ b/plugins/extraction/ExtrOcamlString.v
@@ -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/plugins/extraction/ExtrOcamlZBigInt.v b/plugins/extraction/ExtrOcamlZBigInt.v
index 54b314de..5ca6bd7b 100644
--- a/plugins/extraction/ExtrOcamlZBigInt.v
+++ b/plugins/extraction/ExtrOcamlZBigInt.v
@@ -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/plugins/extraction/ExtrOcamlZInt.v b/plugins/extraction/ExtrOcamlZInt.v
index b302cd36..a7046626 100644
--- a/plugins/extraction/ExtrOcamlZInt.v
+++ b/plugins/extraction/ExtrOcamlZInt.v
@@ -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/plugins/extraction/big.ml b/plugins/extraction/big.ml
index 4c33691d..ae04ba6d 100644
--- a/plugins/extraction/big.ml
+++ b/plugins/extraction/big.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/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 9cea0562..9713fcd2 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.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: common.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: common.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Pp
open Util
@@ -179,6 +179,16 @@ let mktable autoclean =
if autoclean then register_cleanup (fun () -> Hashtbl.clear h);
(Hashtbl.add h, Hashtbl.find h, fun () -> Hashtbl.clear h)
+(* We might have built [global_reference] whose canonical part is
+ inaccurate. We must hence compare only the user part,
+ hence using a Hashtbl might be incorrect *)
+
+let mktable_ref autoclean =
+ let m = ref Refmap'.empty in
+ let clear () = m := Refmap'.empty in
+ if autoclean then register_cleanup clear;
+ (fun r v -> m := Refmap'.add r v !m), (fun r -> Refmap'.find r !m), clear
+
(* A table recording objects in the first level of all MPfile *)
let add_mpfiles_content,get_mpfiles_content,clear_mpfiles_content =
@@ -355,10 +365,10 @@ let ref_renaming_fun (k,r) =
(* Cached version of the last function *)
let ref_renaming =
- let add,get,_ = mktable true in
- fun x ->
- try if is_mp_bound (base_mp (modpath_of_r (snd x))) then raise Not_found; get x
- with Not_found -> let y = ref_renaming_fun x in add x y; y
+ let add,get,_ = mktable_ref true in
+ fun ((k,r) as x) ->
+ try if is_mp_bound (base_mp (modpath_of_r r)) then raise Not_found; get r
+ with Not_found -> let y = ref_renaming_fun x in add r y; y
(* [visible_clash mp0 (k,s)] checks if [mp0-s] of kind [k]
can be printed as [s] in the current context of visible
diff --git a/plugins/extraction/common.mli b/plugins/extraction/common.mli
index f6ff76ba..22bad6cd 100644
--- a/plugins/extraction/common.mli
+++ b/plugins/extraction/common.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: common.mli 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: common.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Names
open Libnames
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 7d4cd770..3fa674d3 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
+(*i $Id: extract_env.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Term
open Declarations
@@ -404,10 +404,18 @@ let print_one_decl struc mp decl =
(*s Extraction of a ml struct to a file. *)
+(** For Recursive Extraction, writing directly on stdout
+ won't work with coqide, we use a buffer instead *)
+
+let buf = Buffer.create 1000
+
let formatter dry file =
let ft =
if dry then Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ())
- else Pp_control.with_output_to (Option.default stdout file)
+ else
+ match file with
+ | Some f -> Pp_control.with_output_to f
+ | None -> Format.formatter_of_buffer buf
in
(* We never want to see ellipsis ... in extracted code *)
Format.pp_set_max_boxes ft max_int;
@@ -421,6 +429,7 @@ let formatter dry file =
ft
let print_structure_to_file (fn,si,mo) dry struc =
+ Buffer.clear buf;
let d = descr () in
reset_renaming_tables AllButExternal;
let unsafe_needs = {
@@ -463,7 +472,12 @@ let print_structure_to_file (fn,si,mo) dry struc =
close_out cout; raise e
end;
info_file si)
- (if dry then None else si)
+ (if dry then None else si);
+ (* Print the buffer content via Coq standard formatter (ok with coqide). *)
+ if Buffer.length buf <> 0 then begin
+ Pp.message (Buffer.contents buf);
+ Buffer.reset buf
+ end
(*********************************************)
diff --git a/plugins/extraction/extract_env.mli b/plugins/extraction/extract_env.mli
index b4516898..145cd6b3 100644
--- a/plugins/extraction/extract_env.mli
+++ b/plugins/extraction/extract_env.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: extract_env.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extract_env.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*s This module declares the extraction commands. *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index b9a3a736..27f32a4a 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.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: extraction.ml 13795 2011-01-22 14:43:06Z glondu $ i*)
+(*i $Id: extraction.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
(*i*)
open Util
@@ -36,9 +36,17 @@ let current_fixpoints = ref ([] : constant list)
let none = Evd.empty
-let type_of env c = Retyping.get_type_of env none (strip_outer_cast c)
+let type_of env c =
+ try
+ let polyprop = (lang() = Haskell) in
+ Retyping.get_type_of ~polyprop env none (strip_outer_cast c)
+ with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
-let sort_of env c = Retyping.get_sort_family_of env none (strip_outer_cast c)
+let sort_of env c =
+ try
+ let polyprop = (lang() = Haskell) in
+ Retyping.get_sort_family_of ~polyprop env none (strip_outer_cast c)
+ with SingletonInductiveBecomesProp id -> error_singleton_become_prop id
let is_axiom env kn = (Environ.lookup_constant kn env).const_body = None
@@ -423,17 +431,16 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let mp,d,_ = repr_mind kn in
let rec select_fields l typs = match l,typs with
| [],[] -> []
- | (Name id)::l, typ::typs ->
- if isDummy (expand env typ) then select_fields l typs
- else
- let knp = make_con mp d (label_of_id id) in
- if List.for_all ((=) Keep) (type2signature env typ)
- then
- projs := Cset.add knp !projs;
- (ConstRef knp) :: (select_fields l typs)
+ | _::l, typ::typs when isDummy (expand env typ) ->
+ select_fields l typs
| Anonymous::l, typ::typs ->
- if isDummy (expand env typ) then select_fields l typs
- else error_record r
+ None :: (select_fields l typs)
+ | Name id::l, typ::typs ->
+ let knp = make_con mp d (label_of_id id) in
+ (* Is it safe to use [id] for projections [foo.id] ? *)
+ if List.for_all ((=) Keep) (type2signature env typ)
+ then projs := Cset.add knp !projs;
+ Some (ConstRef knp) :: (select_fields l typs)
| _ -> assert false
in
let field_glob = select_fields field_names typ
@@ -444,10 +451,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *)
let n = nb_default_params env
(Inductive.type_of_inductive env (mib,mip0))
in
- List.iter
- (Option.iter
- (fun kn -> if Cset.mem kn !projs then add_projection n kn))
- (lookup_projections ip)
+ let check_proj kn = if Cset.mem kn !projs then add_projection n kn in
+ List.iter (Option.iter check_proj) (lookup_projections ip)
with Not_found -> ()
end;
Record field_glob
@@ -561,7 +566,11 @@ let rec extract_term env mle mlt c args =
let a = new_meta () in
let c1' = extract_term env mle a c1 [] in
(* The type of [c1'] is generalized and stored in [mle]. *)
- let mle' = Mlenv.push_gen mle a in
+ let mle' =
+ if generalizable c1'
+ then Mlenv.push_gen mle a
+ else Mlenv.push_type mle a
+ in
MLletin (Id id, c1', extract_term env' mle' mlt c2 args')
with NotDefault d ->
let mle' = Mlenv.push_std_type mle (Tdummy d) in
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 0574b009..8a2125fe 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.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: extraction.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: extraction.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*s Extraction from Coq terms to Miniml. *)
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index fb25e7d1..ebd4de0d 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.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 *)
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 17a38136..aeacef93 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.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: haskell.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: haskell.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*s Production of Haskell syntax. *)
@@ -47,6 +47,7 @@ let preamble mod_name used_modules usf =
(if used_modules = [] then mt () else fnl ()) ++
(if not usf.magic then mt ()
else str "\
+unsafeCoerce :: a -> b
#ifdef __GLASGOW_HASKELL__
import qualified GHC.Base
unsafeCoerce = GHC.Base.unsafeCoerce#
@@ -57,7 +58,8 @@ unsafeCoerce = IOExts.unsafeCoerce
#endif" ++ fnl2 ())
++
(if not usf.mldummy then mt ()
- else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
+ else str "__ :: any" ++ fnl () ++
+ str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
let pp_abst = function
| [] -> (mt ())
diff --git a/plugins/extraction/haskell.mli b/plugins/extraction/haskell.mli
index 0b68e73b..eb774db7 100644
--- a/plugins/extraction/haskell.mli
+++ b/plugins/extraction/haskell.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: haskell.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: haskell.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
val haskell_descr : Miniml.language_descr
diff --git a/plugins/extraction/miniml.mli b/plugins/extraction/miniml.mli
index 20092815..aaf2d0c3 100644
--- a/plugins/extraction/miniml.mli
+++ b/plugins/extraction/miniml.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: miniml.mli 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: miniml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*s Target language for extraction: a core ML called MiniML. *)
@@ -57,7 +57,7 @@ type inductive_kind =
| Singleton
| Coinductive
| Standard
- | Record of global_reference list
+ | Record of global_reference option list (* None for anonymous field *)
(* A [ml_ind_packet] is the miniml counterpart of a [one_inductive_body].
If the inductive is logical ([ip_logical = false]), then all other fields
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index c242e4ab..3c7ee0f2 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.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: mlutil.ml 14003 2011-04-14 23:09:41Z letouzey $ i*)
+(*i $Id: mlutil.ml 14786 2011-12-10 12:55:19Z letouzey $ i*)
(*i*)
open Pp
@@ -119,6 +119,7 @@ let rec mgu = function
mgu (a, a'); mgu (b, b')
| Tglob (r,l), Tglob (r',l') when r = r' ->
List.iter mgu (List.combine l l')
+ | (Tdummy _, _ | _, Tdummy _) when lang() = Haskell -> ()
| Tdummy _, Tdummy _ -> ()
| t, u when t = u -> () (* for Tvar, Tvar', Tunknown, Taxiom *)
| _ -> raise Impossible
@@ -129,6 +130,11 @@ let put_magic_if b a = if b && lang () <> Scheme then MLmagic a else a
let put_magic p a = if needs_magic p && lang () <> Scheme then MLmagic a else a
+let generalizable a =
+ lang () <> Ocaml ||
+ match a with
+ | MLapp _ -> false
+ | _ -> true (* TODO, this is just an approximation for the moment *)
(*S ML type env. *)
@@ -961,10 +967,18 @@ let kill_some_lams bl (ids,c) =
let kill_dummy_lams c =
let ids,c = collect_lams c in
let bl = List.map sign_of_id ids in
- if (List.mem Keep bl) && (List.exists isKill bl) then
- let ids',c = kill_some_lams bl (ids,c) in
- ids, named_lams ids' c
- else raise Impossible
+ if not (List.mem Keep bl) then raise Impossible;
+ let rec fst_kill n = function
+ | [] -> raise Impossible
+ | Kill _ :: bl -> n
+ | Keep :: bl -> fst_kill (n+1) bl
+ in
+ let skip = max 0 ((fst_kill 0 bl) - 1) in
+ let ids_skip, ids = list_chop skip ids in
+ let _, bl = list_chop skip bl in
+ let c = named_lams ids_skip c in
+ let ids',c = kill_some_lams bl (ids,c) in
+ ids, named_lams ids' c
(*s [eta_expansion_sign] takes a function [fun idn ... id1 -> c]
and a signature [s] and builds a eta-long version. *)
@@ -1005,21 +1019,26 @@ let term_expunge s (ids,c) =
MLlam (Dummy, ast_lift 1 c)
else named_lams ids c
-(*s [kill_dummy_args ids t0 t] looks for occurences of [t0] in [t] and
- purge the args of [t0] corresponding to a [dummy_name].
+(*s [kill_dummy_args ids r t] looks for occurences of [MLrel r] in [t] and
+ purge the args of [MLrel r] corresponding to a [dummy_name].
It makes eta-expansion if needed. *)
-let kill_dummy_args ids t0 t =
+let kill_dummy_args ids r t =
let m = List.length ids in
let bl = List.rev_map sign_of_id ids in
+ let rec found n = function
+ | MLrel r' when r' = r + n -> true
+ | MLmagic e -> found n e
+ | _ -> false
+ in
let rec killrec n = function
- | MLapp(e, a) when e = ast_lift n t0 ->
+ | MLapp(e, a) when found n e ->
let k = max 0 (m - (List.length a)) in
let a = List.map (killrec n) a in
let a = List.map (ast_lift k) a in
let a = select_via_bl bl (a @ (eta_args k)) in
named_lams (list_firstn k ids) (MLapp (ast_lift k e, a))
- | e when e = ast_lift n t0 ->
+ | e when found n e ->
let a = select_via_bl bl (eta_args m) in
named_lams ids (MLapp (ast_lift m e, a))
| e -> ast_map_lift killrec n e
@@ -1031,28 +1050,28 @@ let rec kill_dummy = function
| MLfix(i,fi,c) ->
(try
let ids,c = kill_dummy_fix i c in
- ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids (MLrel 1) (MLrel 1))
+ ast_subst (MLfix (i,fi,c)) (kill_dummy_args ids 1 (MLrel 1))
with Impossible -> MLfix (i,fi,Array.map kill_dummy c))
| MLapp (MLfix (i,fi,c),a) ->
let a = List.map kill_dummy a in
(try
let ids,c = kill_dummy_fix i c in
let fake = MLapp (MLrel 1, List.map (ast_lift 1) a) in
- let fake' = kill_dummy_args ids (MLrel 1) fake in
+ let fake' = kill_dummy_args ids 1 fake in
ast_subst (MLfix (i,fi,c)) fake'
with Impossible -> MLapp(MLfix(i,fi,Array.map kill_dummy c),a))
| MLletin(id, MLfix (i,fi,c),e) ->
(try
let ids,c = kill_dummy_fix i c in
- let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in
+ let e = kill_dummy (kill_dummy_args ids 1 e) in
MLletin(id, MLfix(i,fi,c),e)
with Impossible ->
MLletin(id, MLfix(i,fi,Array.map kill_dummy c),kill_dummy e))
| MLletin(id,c,e) ->
(try
let ids,c = kill_dummy_lams (kill_dummy_hd c) in
- let e = kill_dummy (kill_dummy_args ids (MLrel 1) e) in
- let c = eta_red (kill_dummy c) in
+ let e = kill_dummy (kill_dummy_args ids 1 e) in
+ let c = kill_dummy c in
if is_atomic c then ast_subst c e else MLletin (id, c, e)
with Impossible -> MLletin(id,kill_dummy c,kill_dummy e))
| a -> ast_map kill_dummy a
@@ -1064,8 +1083,8 @@ and kill_dummy_hd = function
| MLletin(id,c,e) ->
(try
let ids,c = kill_dummy_lams (kill_dummy_hd c) in
- let e = kill_dummy_hd (kill_dummy_args ids (MLrel 1) e) in
- let c = eta_red (kill_dummy c) in
+ let e = kill_dummy_hd (kill_dummy_args ids 1 e) in
+ let c = kill_dummy c in
if is_atomic c then ast_subst c e else MLletin (id, c, e)
with Impossible -> MLletin(id,kill_dummy c,kill_dummy_hd e))
| a -> a
@@ -1075,7 +1094,7 @@ and kill_dummy_fix i c =
let ids,ci = kill_dummy_lams (kill_dummy_hd c.(i)) in
let c = Array.copy c in c.(i) <- ci;
for j = 0 to (n-1) do
- c.(j) <- kill_dummy (kill_dummy_args ids (MLrel (n-i)) c.(j))
+ c.(j) <- kill_dummy (kill_dummy_args ids (n-i) c.(j))
done;
ids,c
diff --git a/plugins/extraction/mlutil.mli b/plugins/extraction/mlutil.mli
index 6b0cd4f9..54a1baaa 100644
--- a/plugins/extraction/mlutil.mli
+++ b/plugins/extraction/mlutil.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: mlutil.mli 13733 2010-12-21 13:08:53Z letouzey $ i*)
+(*i $Id: mlutil.mli 14786 2011-12-10 12:55:19Z letouzey $ i*)
open Util
open Names
@@ -30,6 +30,8 @@ val needs_magic : ml_type * ml_type -> bool
val put_magic_if : bool -> ml_ast -> ml_ast
val put_magic : ml_type * ml_type -> ml_ast -> ml_ast
+val generalizable : ml_ast -> bool
+
(*s ML type environment. *)
module Mlenv : sig
diff --git a/plugins/extraction/modutil.ml b/plugins/extraction/modutil.ml
index 23ec108a..ffa38def 100644
--- a/plugins/extraction/modutil.ml
+++ b/plugins/extraction/modutil.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: modutil.ml 14006 2011-04-14 23:09:56Z letouzey $ i*)
+(*i $Id: modutil.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Names
open Declarations
@@ -66,7 +66,7 @@ let struct_iter do_decl do_spec s =
type do_ref = global_reference -> unit
let record_iter_references do_term = function
- | Record l -> List.iter do_term l
+ | Record l -> List.iter (Option.iter do_term) l
| _ -> ()
let type_iter_references do_type t =
diff --git a/plugins/extraction/modutil.mli b/plugins/extraction/modutil.mli
index bb405d60..26d07872 100644
--- a/plugins/extraction/modutil.mli
+++ b/plugins/extraction/modutil.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: modutil.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: modutil.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Names
open Declarations
diff --git a/plugins/extraction/ocaml.ml b/plugins/extraction/ocaml.ml
index 81eea9e2..c07a1758 100644
--- a/plugins/extraction/ocaml.ml
+++ b/plugins/extraction/ocaml.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: ocaml.ml 14010 2011-04-15 16:05:07Z letouzey $ i*)
+(*i $Id: ocaml.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*s Production of Ocaml syntax. *)
@@ -113,9 +113,18 @@ let get_infix r =
let s = find_custom r in
String.sub s 1 (String.length s - 2)
-exception NoRecord
+let get_ind = function
+ | IndRef _ as r -> r
+ | ConstructRef (ind,_) -> IndRef ind
+ | _ -> assert false
-let find_projections = function Record l -> l | _ -> raise NoRecord
+let pp_one_field r i = function
+ | Some r -> pp_global Term r
+ | None -> pp_global Type (get_ind r) ++ str "__" ++ int i
+
+let pp_field r fields i = pp_one_field r i (List.nth fields i)
+
+let pp_fields r fields = list_map_i (pp_one_field r) 0 fields
(*s Pretty-printing of types. [par] is a boolean indicating whether parentheses
are needed or not. *)
@@ -202,9 +211,9 @@ let rec pp_expr par env args =
| MLcons (_,r,[]) ->
assert (args=[]);
pp_global Cons r
- | MLcons ({c_kind = Record projs}, r, args') ->
+ | MLcons ({c_kind = Record fields}, r, args') ->
assert (args=[]);
- pp_record_pat (projs, List.map (pp_expr true env []) args')
+ pp_record_pat (pp_fields r fields, List.map (pp_expr true env []) args')
| MLcons (_,r,[arg1;arg2]) when is_infix r ->
assert (args=[]);
pp_par par
@@ -234,25 +243,25 @@ let rec pp_expr par env args =
(pp_expr false env [] t)
in
(try
- let projs = find_projections info.m_kind in
- let (_, ids, c) = pv.(0) in
+ (* First, can this match be printed as a mere record projection ? *)
+ let fields =
+ match info.m_kind with Record f -> f | _ -> raise Impossible
+ in
+ let (r, ids, c) = pv.(0) in
let n = List.length ids in
+ let free_of_patvar a = not (List.exists (ast_occurs_itvl 1 n) a) in
+ let proj_hd i =
+ pp_expr true env [] t ++ str "." ++ pp_field r fields i
+ in
match c with
- | MLrel i when i <= n ->
- apply (pp_par par' (pp_expr true env [] t ++ str "." ++
- pp_global Term (List.nth projs (n-i))))
- | MLapp (MLrel i, a) when i <= n ->
- if List.exists (ast_occurs_itvl 1 n) a
- then raise NoRecord
- else
- let ids,env' = push_vars (List.rev_map id_of_mlid ids) env
- in
- (pp_apply
- (pp_expr true env [] t ++ str "." ++
- pp_global Term (List.nth projs (n-i)))
- par ((List.map (pp_expr true env' []) a) @ args))
- | _ -> raise NoRecord
- with NoRecord ->
+ | MLrel i when i <= n -> apply (pp_par par' (proj_hd (n-i)))
+ | MLapp (MLrel i, a) when (i <= n) && (free_of_patvar a) ->
+ let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
+ (pp_apply (proj_hd (n-i))
+ par ((List.map (pp_expr true env' []) a) @ args))
+ | _ -> raise Impossible
+ with Impossible ->
+ (* Second, can this match be printed as a let-in ? *)
if Array.length pv = 1 then
let s1,s2 = pp_one_pat env info pv.(0) in
apply
@@ -263,6 +272,7 @@ let rec pp_expr par env args =
++ spc () ++ str "in") ++
spc () ++ hov 0 s2)))
else
+ (* Otherwise, standard match *)
apply
(pp_par par'
(try pp_ifthenelse par' env expr pv
@@ -283,11 +293,11 @@ let rec pp_expr par env args =
pp_par par (str "failwith \"AXIOM TO BE REALIZED\"")
-and pp_record_pat (projs, args) =
+and pp_record_pat (fields, args) =
str "{ " ++
prlist_with_sep (fun () -> str ";" ++ spc ())
- (fun (r,a) -> pp_global Term r ++ str " =" ++ spc () ++ a)
- (List.combine projs args) ++
+ (fun (f,a) -> f ++ str " =" ++ spc () ++ a)
+ (List.combine fields args) ++
str " }"
and pp_ifthenelse par env expr pv = match pv with
@@ -304,18 +314,18 @@ and pp_ifthenelse par env expr pv = match pv with
and pp_one_pat env info (r,ids,t) =
let ids,env' = push_vars (List.rev_map id_of_mlid ids) env in
let expr = pp_expr (expr_needs_par t) env' [] t in
- try
- let projs = find_projections info.m_kind in
- pp_record_pat (projs, List.rev_map pr_id ids), expr
- with NoRecord ->
- (match List.rev ids with
- | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
- | [] -> pp_global Cons r
- | ids ->
+ let patt = match info.m_kind with
+ | Record fields ->
+ pp_record_pat (pp_fields r fields, List.rev_map pr_id ids)
+ | _ -> match List.rev ids with
+ | [i1;i2] when is_infix r -> pr_id i1 ++ str (get_infix r) ++ pr_id i2
+ | [] -> pp_global Cons r
+ | ids ->
(* hack Extract Inductive prod *)
(if str_global Cons r = "" then mt () else pp_global Cons r ++ spc ())
- ++ pp_boxed_tuple pr_id ids),
- expr
+ ++ pp_boxed_tuple pr_id ids
+ in
+ patt, expr
and pp_pat env info pv =
let factor_br, factor_set = try match info.m_same with
@@ -448,10 +458,11 @@ let pp_singleton kn packet =
pp_comment (str "singleton inductive, whose constructor was " ++
pr_id packet.ip_consnames.(0)))
-let pp_record kn projs ip_equiv packet =
- let name = pp_global Type (IndRef (mind_of_kn kn,0)) in
- let projnames = List.map (pp_global Term) projs in
- let l = List.combine projnames packet.ip_types.(0) in
+let pp_record kn fields ip_equiv packet =
+ let ind = IndRef (mind_of_kn kn,0) in
+ let name = pp_global Type ind in
+ let fieldnames = pp_fields ind fields in
+ let l = List.combine fieldnames packet.ip_types.(0) in
let pl = rename_tvars keywords packet.ip_vars in
str "type " ++ pp_parameters pl ++ name ++
pp_equiv pl name ip_equiv ++ str " = { "++
@@ -512,8 +523,7 @@ let pp_mind kn i =
match i.ind_kind with
| Singleton -> pp_singleton kn i.ind_packets.(0)
| Coinductive -> pp_ind true kn i
- | Record projs ->
- pp_record kn projs (i.ind_equiv,0) i.ind_packets.(0)
+ | Record fields -> pp_record kn fields (i.ind_equiv,0) i.ind_packets.(0)
| Standard -> pp_ind false kn i
let pp_decl = function
diff --git a/plugins/extraction/ocaml.mli b/plugins/extraction/ocaml.mli
index 477b4351..c0b4e5b3 100644
--- a/plugins/extraction/ocaml.mli
+++ b/plugins/extraction/ocaml.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: ocaml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: ocaml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
val ocaml_descr : Miniml.language_descr
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index cb980cba..1f04ca59 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.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: scheme.ml 14006 2011-04-14 23:09:56Z letouzey $ i*)
+(*i $Id: scheme.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*s Production of Scheme syntax. *)
diff --git a/plugins/extraction/scheme.mli b/plugins/extraction/scheme.mli
index e413d31e..c7c3d8b5 100644
--- a/plugins/extraction/scheme.mli
+++ b/plugins/extraction/scheme.mli
@@ -1,11 +1,11 @@
(************************************************************************)
(* 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: scheme.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: scheme.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
val scheme_descr : Miniml.language_descr
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml
index b2b5e6f5..67cf2210 100644
--- a/plugins/extraction/table.ml
+++ b/plugins/extraction/table.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: table.ml 14012 2011-04-15 16:45:27Z letouzey $ i*)
+(*i $Id: table.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Names
open Term
@@ -21,10 +21,21 @@ open Util
open Pp
open Miniml
-(** Sets and maps for [global_reference] that do _not_ work modulo
- name equivalence (otherwise use Refset / Refmap ) *)
+(** Sets and maps for [global_reference] that work modulo equivalent
+ on the user part of the name (otherwise use Refset / Refmap ) *)
+
+module RefOrd = struct
+ type t = global_reference
+ let compare x y =
+ let make_name = function
+ | ConstRef con -> ConstRef(constant_of_kn(user_con con))
+ | IndRef (kn,i) -> IndRef(mind_of_kn(user_mind kn),i)
+ | ConstructRef ((kn,i),j)-> ConstructRef((mind_of_kn(user_mind kn),i),j)
+ | VarRef id -> VarRef id
+ in
+ Pervasives.compare (make_name x) (make_name y)
+end
-module RefOrd = struct type t = global_reference let compare = compare end
module Refmap' = Map.Make(RefOrd)
module Refset' = Set.Make(RefOrd)
@@ -316,6 +327,15 @@ let error_no_module_expr mp =
++ str "some Declare Module outside any Module Type.\n"
++ str "This situation is currently unsupported by the extraction.")
+let error_singleton_become_prop id =
+ err (str "The informative inductive type " ++ pr_id id ++
+ str " has a Prop instance.\n" ++
+ str "This happens when a sort-polymorphic singleton inductive type\n" ++
+ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++
+ str "The Ocaml extraction cannot handle this situation yet.\n" ++
+ str "Instead, use a sort-monomorphic type such as (True /\\ True)\n" ++
+ str "or extract to Haskell.")
+
let error_unknown_module m =
err (str "Module" ++ spc () ++ pr_qualid m ++ spc () ++ str "not found.")
@@ -335,10 +355,6 @@ let error_MPfile_as_mod mp b =
"Monolithic Extraction cannot deal with this situation.\n"^
"Please "^s2^"use (Recursive) Extraction Library instead.\n"))
-let error_record r =
- err (str "Record " ++ safe_pr_global r ++ str " has an anonymous field." ++
- fnl () ++ str "To help extraction, please use an explicit name.")
-
let msg_non_implicit r n id =
let name = match id with
| Anonymous -> ""
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli
index 2eafe1d8..b70d3efa 100644
--- a/plugins/extraction/table.mli
+++ b/plugins/extraction/table.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: table.mli 14012 2011-04-15 16:45:27Z letouzey $ i*)
+(*i $Id: table.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Names
open Libnames
@@ -30,11 +30,11 @@ val error_inductive : global_reference -> 'a
val error_nb_cons : unit -> 'a
val error_module_clash : module_path -> module_path -> 'a
val error_no_module_expr : module_path -> 'a
+val error_singleton_become_prop : identifier -> 'a
val error_unknown_module : qualid -> 'a
val error_scheme : unit -> 'a
val error_not_visible : global_reference -> 'a
val error_MPfile_as_mod : module_path -> bool -> 'a
-val error_record : global_reference -> 'a
val check_inside_module : unit -> unit
val check_inside_section : unit -> unit
val check_loaded_modfile : module_path -> unit
diff --git a/plugins/field/LegacyField.v b/plugins/field/LegacyField.v
index 6c825353..9017f8d5 100644
--- a/plugins/field/LegacyField.v
+++ b/plugins/field/LegacyField.v
@@ -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: LegacyField.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyField.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export LegacyField_Compl.
Require Export LegacyField_Theory.
diff --git a/plugins/field/LegacyField_Compl.v b/plugins/field/LegacyField_Compl.v
index a3b46900..52e049a5 100644
--- a/plugins/field/LegacyField_Compl.v
+++ b/plugins/field/LegacyField_Compl.v
@@ -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: LegacyField_Compl.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyField_Compl.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import List.
diff --git a/plugins/field/LegacyField_Tactic.v b/plugins/field/LegacyField_Tactic.v
index 9c92e38a..f6626e4a 100644
--- a/plugins/field/LegacyField_Tactic.v
+++ b/plugins/field/LegacyField_Tactic.v
@@ -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: LegacyField_Tactic.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyField_Tactic.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import List.
Require Import LegacyRing.
diff --git a/plugins/field/LegacyField_Theory.v b/plugins/field/LegacyField_Theory.v
index 2407026f..8d10bc8e 100644
--- a/plugins/field/LegacyField_Theory.v
+++ b/plugins/field/LegacyField_Theory.v
@@ -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: LegacyField_Theory.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyField_Theory.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import List.
Require Import Peano_dec.
diff --git a/plugins/field/field.ml4 b/plugins/field/field.ml4
index 47f52370..37aa457d 100644
--- a/plugins/field/field.ml4
+++ b/plugins/field/field.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: field.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: field.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Names
open Pp
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index d039a930..1f3fd595 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.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: formula.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: formula.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Hipattern
open Names
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index fbb103c0..a831c087 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: formula.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: formula.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Names
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 19b63407..8e68506c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.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: g_ground.ml4 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: g_ground.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Formula
open Sequent
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 354bcda2..163b9891 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.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: ground.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ground.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Formula
open Sequent
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index ba8051da..8328bb3a 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ground.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ground.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
val ground_tac: Tacmach.tactic ->
(Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 714604ae..4802aaa3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.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: instances.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: instances.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Formula
open Sequent
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 8b913719..537e40e7 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.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: instances.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: instances.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Term
open Tacmach
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 9cff67dc..e6d73fb6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.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: rules.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: rules.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Names
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index ec6d2bd0..a5a6b614 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: rules.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Tacmach
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1d439693..faac286e 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.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: sequent.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: sequent.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Util
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 1232f1e8..ef052605 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sequent.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: sequent.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Util
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 835b0409..4e0ad108 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.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: unify.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: unify.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Util
open Formula
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index af2ce01d..4e0d88d3 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unify.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: unify.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 05e85cde..d6447111 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -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: Fourier.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Fourier.v 14641 2011-11-06 11:59:10Z herbelin $ *)
(* "Fourier's method to solve linear inequations/equations systems.".*)
diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
index 3cd26cb8..7c5b5ed7 100644
--- a/plugins/fourier/Fourier_util.v
+++ b/plugins/fourier/Fourier_util.v
@@ -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: Fourier_util.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Fourier_util.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export Rbase.
Comments "Lemmas used by the tactic Fourier".
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 16123fd7..1a92c716 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.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: fourier.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: fourier.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* Méthode d'élimination de Fourier *)
(* Référence:
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index e9392e78..2cabcf52 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.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: fourierR.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: fourierR.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index d3b8228d..ea766830 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.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: g_fourier.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_fourier.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open FourierR
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index b29b8362..763ed82f 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -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/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index e47f19bf..41fafdf1 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.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 *)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 84470a0f..aa42f6cd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.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 *)
@@ -504,6 +504,15 @@ and intros_with_rewrite_aux : tactic =
intros_with_rewrite
]
g
+ else if isVar args.(2)
+ then
+ let id = pf_get_new_id (id_of_string "y") g in
+ tclTHENSEQ [ h_intro id;
+ generalize_dependent_of (destVar args.(2)) id;
+ tclTRY (Equality.rewriteRL (mkVar id));
+ intros_with_rewrite
+ ]
+ g
else
begin
let id = pf_get_new_id (id_of_string "y") g in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 799180b7..40ee116d 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.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/plugins/funind/rawterm_to_relation.ml b/plugins/funind/rawterm_to_relation.ml
index 3c3a36f0..b74422a3 100644
--- a/plugins/funind/rawterm_to_relation.ml
+++ b/plugins/funind/rawterm_to_relation.ml
@@ -716,11 +716,11 @@ and build_entry_lc_from_case env funname make_discr
*)
let case_resl =
List.fold_right
- (fun (case_arg,_) ctxt_argsl ->
- let arg_res = build_entry_lc env funname avoid case_arg in
- combine_results combine_args arg_res ctxt_argsl
- )
- el
+ (fun (case_arg,_) ctxt_argsl ->
+ let arg_res = build_entry_lc env funname avoid case_arg in
+ combine_results combine_args arg_res ctxt_argsl
+ )
+ el
(mk_result [] [] avoid)
in
let types =
@@ -876,6 +876,32 @@ let is_res id =
with Invalid_argument _ -> false
+
+let same_raw_term rt1 rt2 =
+ match rt1,rt2 with
+ | RRef(_,r1), RRef (_,r2) -> r1=r2
+ | RHole _, RHole _ -> true
+ | _ -> false
+let decompose_raw_eq lhs rhs =
+ let rec decompose_raw_eq lhs rhs acc =
+ observe (str "decomposing eq for " ++ pr_rawconstr lhs ++ str " " ++ pr_rawconstr rhs);
+ let (rhd,lrhs) = raw_decompose_app rhs in
+ let (lhd,llhs) = raw_decompose_app lhs in
+ observe (str "lhd := " ++ pr_rawconstr lhd);
+ observe (str "rhd := " ++ pr_rawconstr rhd);
+ observe (str "llhs := " ++ int (List.length llhs));
+ observe (str "lrhs := " ++ int (List.length lrhs));
+ let sllhs = List.length llhs in
+ let slrhs = List.length lrhs in
+ if same_raw_term lhd rhd && sllhs = slrhs
+ then
+ (* let _ = assert false in *)
+ List.fold_right2 decompose_raw_eq llhs lrhs acc
+ else (lhs,rhs)::acc
+ in
+ decompose_raw_eq lhs rhs []
+
+
exception Continue
(*
The second phase which reconstruct the real type of the constructor.
@@ -1032,6 +1058,41 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
mkRProd(n,t,new_b),id_to_exclude
else new_b, Idset.add id id_to_exclude
*)
+ | RApp(loc1,RRef(loc2,eq_as_ref),[ty;rt1;rt2])
+ when eq_as_ref = Lazy.force Coqlib.coq_eq_ref && n = Anonymous
+ ->
+ begin
+ try
+ let l = decompose_raw_eq rt1 rt2 in
+ if List.length l > 1
+ then
+ let new_rt =
+ List.fold_left
+ (fun acc (lhs,rhs) ->
+ mkRProd(Anonymous,
+ mkRApp(mkRRef(eq_as_ref),[mkRHole ();lhs;rhs]),acc)
+ )
+ b
+ l
+ in
+ rebuild_cons env nb_args relname args crossed_types depth new_rt
+ else raise Continue
+ with Continue ->
+ observe (str "computing new type for prod : " ++ pr_rawconstr rt);
+ let t' = Pretyping.Default.understand Evd.empty env t in
+ let new_env = Environ.push_rel (n,None,t') env in
+ let new_b,id_to_exclude =
+ rebuild_cons new_env
+ nb_args relname
+ args new_crossed_types
+ (depth + 1) b
+ in
+ match n with
+ | Name id when Idset.mem id id_to_exclude && depth >= nb_args ->
+ new_b,Idset.remove id
+ (Idset.filter not_free_in_t id_to_exclude)
+ | _ -> mkRProd(n,t,new_b),Idset.filter not_free_in_t id_to_exclude
+ end
| _ ->
observe (str "computing new type for prod : " ++ pr_rawconstr rt);
let t' = Pretyping.Default.understand Evd.empty env t in
@@ -1122,12 +1183,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
(* debuging wrapper *)
let rebuild_cons env nb_args relname args crossed_types rt =
-(* observennl (str "rebuild_cons : rt := "++ pr_rawconstr rt ++ *)
-(* str "nb_args := " ++ str (string_of_int nb_args)); *)
+ observe (str "rebuild_cons : rt := "++ pr_rawconstr rt ++
+ str "nb_args := " ++ str (string_of_int nb_args));
let res =
rebuild_cons env nb_args relname args crossed_types 0 rt
in
-(* observe (str " leads to "++ pr_rawconstr (fst res)); *)
+ observe (str " leads to "++ pr_rawconstr (fst res));
res
@@ -1266,7 +1327,7 @@ let do_build_inductive
(function result (* (args',concl') *) ->
let rt = compose_raw_context result.context result.value in
let nb_args = List.length funsargs.(i) in
- (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
+ (* with_full_print (fun rt -> Pp.msgnl (str "raw constr " ++ pr_rawconstr rt)) rt; *)
fst (
rebuild_cons env_with_graphs nb_args relnames.(i)
[]
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 9c4cc78a..83868da9 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.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 *)
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: recdef.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: recdef.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Termops
diff --git a/plugins/micromega/CheckerMaker.v b/plugins/micromega/CheckerMaker.v
index 8ccc3aa3..8f0f86c5 100644
--- a/plugins/micromega/CheckerMaker.v
+++ b/plugins/micromega/CheckerMaker.v
@@ -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/plugins/micromega/Env.v b/plugins/micromega/Env.v
index 87af9208..5aa30fed 100644
--- a/plugins/micromega/Env.v
+++ b/plugins/micromega/Env.v
@@ -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/plugins/micromega/EnvRing.v b/plugins/micromega/EnvRing.v
index ecffce83..8968a014 100644
--- a/plugins/micromega/EnvRing.v
+++ b/plugins/micromega/EnvRing.v
@@ -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/plugins/micromega/MExtraction.v b/plugins/micromega/MExtraction.v
index 5e03d5b2..5afe7e37 100644
--- a/plugins/micromega/MExtraction.v
+++ b/plugins/micromega/MExtraction.v
@@ -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/plugins/micromega/OrderedRing.v b/plugins/micromega/OrderedRing.v
index 97517957..e4f91fb6 100644
--- a/plugins/micromega/OrderedRing.v
+++ b/plugins/micromega/OrderedRing.v
@@ -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/plugins/micromega/Psatz.v b/plugins/micromega/Psatz.v
index c2c7de70..fde0f29a 100644
--- a/plugins/micromega/Psatz.v
+++ b/plugins/micromega/Psatz.v
@@ -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/plugins/micromega/QMicromega.v b/plugins/micromega/QMicromega.v
index e0056c5f..5ff6a1a7 100644
--- a/plugins/micromega/QMicromega.v
+++ b/plugins/micromega/QMicromega.v
@@ -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/plugins/micromega/RMicromega.v b/plugins/micromega/RMicromega.v
index 2b6ef8c5..305d553c 100644
--- a/plugins/micromega/RMicromega.v
+++ b/plugins/micromega/RMicromega.v
@@ -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/plugins/micromega/Refl.v b/plugins/micromega/Refl.v
index b839195c..53413b4a 100644
--- a/plugins/micromega/Refl.v
+++ b/plugins/micromega/Refl.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* 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/plugins/micromega/RingMicromega.v b/plugins/micromega/RingMicromega.v
index 4dc65f9c..b10cf784 100644
--- a/plugins/micromega/RingMicromega.v
+++ b/plugins/micromega/RingMicromega.v
@@ -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/plugins/micromega/Tauto.v b/plugins/micromega/Tauto.v
index fcbf7f96..0706611c 100644
--- a/plugins/micromega/Tauto.v
+++ b/plugins/micromega/Tauto.v
@@ -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/plugins/micromega/VarMap.v b/plugins/micromega/VarMap.v
index c1358e6f..7d25524a 100644
--- a/plugins/micromega/VarMap.v
+++ b/plugins/micromega/VarMap.v
@@ -1,7 +1,7 @@
(* -*- coding: utf-8 -*- *)
(************************************************************************)
(* 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/plugins/micromega/ZCoeff.v b/plugins/micromega/ZCoeff.v
index f8df9748..cf2bca49 100644
--- a/plugins/micromega/ZCoeff.v
+++ b/plugins/micromega/ZCoeff.v
@@ -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/plugins/micromega/ZMicromega.v b/plugins/micromega/ZMicromega.v
index c8d32473..d6245681 100644
--- a/plugins/micromega/ZMicromega.v
+++ b/plugins/micromega/ZMicromega.v
@@ -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/plugins/micromega/certificate.ml b/plugins/micromega/certificate.ml
index 6fd41ff0..bcab73ec 100644
--- a/plugins/micromega/certificate.ml
+++ b/plugins/micromega/certificate.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/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 6376d023..4eb26afd 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.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/plugins/micromega/csdpcert.ml b/plugins/micromega/csdpcert.ml
index f5314df5..3b47007c 100644
--- a/plugins/micromega/csdpcert.ml
+++ b/plugins/micromega/csdpcert.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/plugins/micromega/g_micromega.ml4 b/plugins/micromega/g_micromega.ml4
index 3b667bf6..9b6842bd 100644
--- a/plugins/micromega/g_micromega.ml4
+++ b/plugins/micromega/g_micromega.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 *)
@@ -14,7 +14,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_micromega.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_micromega.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Quote
open Ring
diff --git a/plugins/micromega/mutils.ml b/plugins/micromega/mutils.ml
index 57f7701e..ef23b912 100644
--- a/plugins/micromega/mutils.ml
+++ b/plugins/micromega/mutils.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/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cd045e42..b48fa36b 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.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/plugins/micromega/sos.mli b/plugins/micromega/sos.mli
index 3d907e19..23219be2 100644
--- a/plugins/micromega/sos.mli
+++ b/plugins/micromega/sos.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/plugins/micromega/sos_types.ml b/plugins/micromega/sos_types.ml
index 91aa5855..6bd463ef 100644
--- a/plugins/micromega/sos_types.ml
+++ b/plugins/micromega/sos_types.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/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v
index aa32b386..ac321ba2 100644
--- a/plugins/nsatz/Nsatz.v
+++ b/plugins/nsatz/Nsatz.v
@@ -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/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml
index 84a05f0e..5fde2cfc 100644
--- a/plugins/nsatz/ideal.ml
+++ b/plugins/nsatz/ideal.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/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4
index 8de3c107..da0ee898 100644
--- a/plugins/nsatz/nsatz.ml4
+++ b/plugins/nsatz/nsatz.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 *)
diff --git a/plugins/nsatz/polynom.ml b/plugins/nsatz/polynom.ml
index b8210bd3..ee7b9f33 100644
--- a/plugins/nsatz/polynom.ml
+++ b/plugins/nsatz/polynom.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/plugins/nsatz/polynom.mli b/plugins/nsatz/polynom.mli
index b82b43b1..980a8306 100644
--- a/plugins/nsatz/polynom.mli
+++ b/plugins/nsatz/polynom.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/plugins/omega/Omega.v b/plugins/omega/Omega.v
index fadecf5d..c8a06265 100644
--- a/plugins/omega/Omega.v
+++ b/plugins/omega/Omega.v
@@ -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 *)
@@ -13,7 +13,7 @@
(* *)
(**************************************************************************)
-(* $Id: Omega.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Omega.v 14641 2011-11-06 11:59:10Z herbelin $ *)
(* We do not require [ZArith] anymore, but only what's necessary for Omega *)
Require Export ZArith_base.
diff --git a/plugins/omega/OmegaPlugin.v b/plugins/omega/OmegaPlugin.v
index ee942db0..69a6ea72 100644
--- a/plugins/omega/OmegaPlugin.v
+++ b/plugins/omega/OmegaPlugin.v
@@ -1,11 +1,11 @@
(************************************************************************)
(* 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: OmegaPlugin.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: OmegaPlugin.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Declare ML Module "omega_plugin".
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e3f9a309..20565d06 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.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 *)
@@ -13,7 +13,7 @@
(* *)
(**************************************************************************)
-(* $Id: coq_omega.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: coq_omega.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Pp
diff --git a/plugins/omega/g_omega.ml4 b/plugins/omega/g_omega.ml4
index eefa67ec..cd6472c3 100644
--- a/plugins/omega/g_omega.ml4
+++ b/plugins/omega/g_omega.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 *)
@@ -15,7 +15,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_omega.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_omega.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Coq_omega
open Refiner
diff --git a/plugins/omega/omega.ml b/plugins/omega/omega.ml
index 9ae0205a..8bb10194 100644
--- a/plugins/omega/omega.ml
+++ b/plugins/omega/omega.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/plugins/quote/Quote.v b/plugins/quote/Quote.v
index b7cc13ae..55bb8bae 100644
--- a/plugins/quote/Quote.v
+++ b/plugins/quote/Quote.v
@@ -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: Quote.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Quote.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Declare ML Module "quote_plugin".
diff --git a/plugins/quote/g_quote.ml4 b/plugins/quote/g_quote.ml4
index 83bfb6ed..3c51223a 100644
--- a/plugins/quote/g_quote.ml4
+++ b/plugins/quote/g_quote.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: g_quote.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_quote.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Tacexpr
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index b6ca770e..baba7e1b 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.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: quote.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: quote.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* The `Quote' tactic *)
diff --git a/plugins/ring/LegacyArithRing.v b/plugins/ring/LegacyArithRing.v
index 3e30b90f..2de16bc1 100644
--- a/plugins/ring/LegacyArithRing.v
+++ b/plugins/ring/LegacyArithRing.v
@@ -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: LegacyArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
(* Instantiation of the Ring tactic for the naturals of Arith $*)
diff --git a/plugins/ring/LegacyNArithRing.v b/plugins/ring/LegacyNArithRing.v
index 337c3085..ae7e62e0 100644
--- a/plugins/ring/LegacyNArithRing.v
+++ b/plugins/ring/LegacyNArithRing.v
@@ -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: LegacyNArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyNArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
(* Instantiation of the Ring tactic for the binary natural numbers *)
diff --git a/plugins/ring/LegacyRing.v b/plugins/ring/LegacyRing.v
index 6b655134..e53e60d3 100644
--- a/plugins/ring/LegacyRing.v
+++ b/plugins/ring/LegacyRing.v
@@ -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: LegacyRing.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export Bool.
Require Export LegacyRing_theory.
diff --git a/plugins/ring/LegacyRing_theory.v b/plugins/ring/LegacyRing_theory.v
index fb4c87fb..bf61aee1 100644
--- a/plugins/ring/LegacyRing_theory.v
+++ b/plugins/ring/LegacyRing_theory.v
@@ -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: LegacyRing_theory.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyRing_theory.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export Bool.
diff --git a/plugins/ring/LegacyZArithRing.v b/plugins/ring/LegacyZArithRing.v
index 22fa87c8..d1412104 100644
--- a/plugins/ring/LegacyZArithRing.v
+++ b/plugins/ring/LegacyZArithRing.v
@@ -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: LegacyZArithRing.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: LegacyZArithRing.v 14641 2011-11-06 11:59:10Z herbelin $ *)
(* Instantiation of the Ring tactic for the binary integers of ZArith *)
diff --git a/plugins/ring/Ring_abstract.v b/plugins/ring/Ring_abstract.v
index e65e1ce8..e6e2dda9 100644
--- a/plugins/ring/Ring_abstract.v
+++ b/plugins/ring/Ring_abstract.v
@@ -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: Ring_abstract.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Ring_abstract.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import LegacyRing_theory.
Require Import Quote.
diff --git a/plugins/ring/Ring_normalize.v b/plugins/ring/Ring_normalize.v
index d68fef4f..dd4e7314 100644
--- a/plugins/ring/Ring_normalize.v
+++ b/plugins/ring/Ring_normalize.v
@@ -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: Ring_normalize.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Ring_normalize.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import LegacyRing_theory.
Require Import Quote.
diff --git a/plugins/ring/Setoid_ring.v b/plugins/ring/Setoid_ring.v
index 3a3dfe84..da4e3756 100644
--- a/plugins/ring/Setoid_ring.v
+++ b/plugins/ring/Setoid_ring.v
@@ -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: Setoid_ring.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Setoid_ring.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export Setoid_ring_theory.
Require Export Quote.
diff --git a/plugins/ring/Setoid_ring_normalize.v b/plugins/ring/Setoid_ring_normalize.v
index 6a53b519..c4527cfb 100644
--- a/plugins/ring/Setoid_ring_normalize.v
+++ b/plugins/ring/Setoid_ring_normalize.v
@@ -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: Setoid_ring_normalize.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Setoid_ring_normalize.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Import Setoid_ring_theory.
Require Import Quote.
diff --git a/plugins/ring/Setoid_ring_theory.v b/plugins/ring/Setoid_ring_theory.v
index d55f25fc..f07cbaf6 100644
--- a/plugins/ring/Setoid_ring_theory.v
+++ b/plugins/ring/Setoid_ring_theory.v
@@ -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: Setoid_ring_theory.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Setoid_ring_theory.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export Bool.
Require Export Setoid.
diff --git a/plugins/ring/g_ring.ml4 b/plugins/ring/g_ring.ml4
index 7fda4920..c5a33f39 100644
--- a/plugins/ring/g_ring.ml4
+++ b/plugins/ring/g_ring.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: g_ring.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: g_ring.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Quote
open Ring
diff --git a/plugins/ring/ring.ml b/plugins/ring/ring.ml
index 3cdf0117..6e67272c 100644
--- a/plugins/ring/ring.ml
+++ b/plugins/ring/ring.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: ring.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ring.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* ML part of the Ring tactic *)
diff --git a/plugins/rtauto/Bintree.v b/plugins/rtauto/Bintree.v
index a62a0780..39c29a3d 100644
--- a/plugins/rtauto/Bintree.v
+++ b/plugins/rtauto/Bintree.v
@@ -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: Bintree.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Bintree.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export List.
Require Export BinPos.
diff --git a/plugins/rtauto/Rtauto.v b/plugins/rtauto/Rtauto.v
index ffa619d0..3817f98c 100644
--- a/plugins/rtauto/Rtauto.v
+++ b/plugins/rtauto/Rtauto.v
@@ -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: Rtauto.v 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: Rtauto.v 14641 2011-11-06 11:59:10Z herbelin $ *)
Require Export List.
diff --git a/plugins/rtauto/g_rtauto.ml4 b/plugins/rtauto/g_rtauto.ml4
index 22f8ca2a..552f23f6 100644
--- a/plugins/rtauto/g_rtauto.ml4
+++ b/plugins/rtauto/g_rtauto.ml4
@@ -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: g_rtauto.ml4 13323 2010-07-24 15:57:30Z herbelin $*)
+(* $Id: g_rtauto.ml4 14641 2011-11-06 11:59:10Z herbelin $*)
(*i camlp4deps: "parsing/grammar.cma" i*)
diff --git a/plugins/rtauto/proof_search.ml b/plugins/rtauto/proof_search.ml
index 23530ef8..500138cf 100644
--- a/plugins/rtauto/proof_search.ml
+++ b/plugins/rtauto/proof_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: proof_search.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: proof_search.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Util
diff --git a/plugins/rtauto/proof_search.mli b/plugins/rtauto/proof_search.mli
index 685a3059..4d77a057 100644
--- a/plugins/rtauto/proof_search.mli
+++ b/plugins/rtauto/proof_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 *)
(************************************************************************)
-(* $Id: proof_search.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: proof_search.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
type form=
Atom of int
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index e079a83c..20b4c8f6 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.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: refl_tauto.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: refl_tauto.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
module Search = Explore.Make(Proof_search)
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 2ff45f57..085a45a5 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -1,11 +1,11 @@
(************************************************************************)
(* 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: refl_tauto.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: refl_tauto.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
(* raises Not_found if no proof is found *)
diff --git a/plugins/setoid_ring/ArithRing.v b/plugins/setoid_ring/ArithRing.v
index 0d4b86b6..6998b656 100644
--- a/plugins/setoid_ring/ArithRing.v
+++ b/plugins/setoid_ring/ArithRing.v
@@ -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/plugins/setoid_ring/BinList.v b/plugins/setoid_ring/BinList.v
index 7128280a..905625cc 100644
--- a/plugins/setoid_ring/BinList.v
+++ b/plugins/setoid_ring/BinList.v
@@ -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/plugins/setoid_ring/Field.v b/plugins/setoid_ring/Field.v
index 90f2f497..6a755af2 100644
--- a/plugins/setoid_ring/Field.v
+++ b/plugins/setoid_ring/Field.v
@@ -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/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v
index da42bbd9..eee89e61 100644
--- a/plugins/setoid_ring/Field_tac.v
+++ b/plugins/setoid_ring/Field_tac.v
@@ -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/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index 84adad25..ccdec656 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -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/plugins/setoid_ring/InitialRing.v b/plugins/setoid_ring/InitialRing.v
index 0d60719f..026e70c8 100644
--- a/plugins/setoid_ring/InitialRing.v
+++ b/plugins/setoid_ring/InitialRing.v
@@ -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/plugins/setoid_ring/NArithRing.v b/plugins/setoid_ring/NArithRing.v
index 1c338bc0..8d7cb0ea 100644
--- a/plugins/setoid_ring/NArithRing.v
+++ b/plugins/setoid_ring/NArithRing.v
@@ -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/plugins/setoid_ring/Ring.v b/plugins/setoid_ring/Ring.v
index c44c2edf..7b48f590 100644
--- a/plugins/setoid_ring/Ring.v
+++ b/plugins/setoid_ring/Ring.v
@@ -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/plugins/setoid_ring/Ring_base.v b/plugins/setoid_ring/Ring_base.v
index 6d4360d6..9bc95a7f 100644
--- a/plugins/setoid_ring/Ring_base.v
+++ b/plugins/setoid_ring/Ring_base.v
@@ -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/plugins/setoid_ring/Ring_polynom.v b/plugins/setoid_ring/Ring_polynom.v
index 43d81809..d33a095f 100644
--- a/plugins/setoid_ring/Ring_polynom.v
+++ b/plugins/setoid_ring/Ring_polynom.v
@@ -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/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v
index 581cf925..4fbdcbaa 100644
--- a/plugins/setoid_ring/Ring_theory.v
+++ b/plugins/setoid_ring/Ring_theory.v
@@ -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/plugins/setoid_ring/ZArithRing.v b/plugins/setoid_ring/ZArithRing.v
index 92a75392..362542b9 100644
--- a/plugins/setoid_ring/ZArithRing.v
+++ b/plugins/setoid_ring/ZArithRing.v
@@ -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/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 8940e565..820246af 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.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*)
-(*i $Id: newring.ml4 13332 2010-07-26 22:12:43Z msozeau $ i*)
+(*i $Id: newring.ml4 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Pp
open Util
diff --git a/plugins/subtac/eterm.mli b/plugins/subtac/eterm.mli
index 2abc25a3..b4bbe3d5 100644
--- a/plugins/subtac/eterm.mli
+++ b/plugins/subtac/eterm.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: eterm.mli 13693 2010-12-08 15:32:25Z msozeau $ i*)
+(*i $Id: eterm.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Environ
open Tacmach
open Term
diff --git a/plugins/subtac/g_subtac.ml4 b/plugins/subtac/g_subtac.ml4
index cd8708d5..ce6d12be 100644
--- a/plugins/subtac/g_subtac.ml4
+++ b/plugins/subtac/g_subtac.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 *)
@@ -14,7 +14,7 @@
Syntax for the subtac terms and types.
Elaborated from correctness/psyntax.ml4 by Jean-Christophe Filliātre *)
-(* $Id: g_subtac.ml4 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: g_subtac.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Flags
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 90b409ba..95cacc38 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.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: subtac.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: subtac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Global
open Pp
diff --git a/plugins/subtac/subtac_cases.ml b/plugins/subtac/subtac_cases.ml
index 866e6a10..25aec39c 100644
--- a/plugins/subtac/subtac_cases.ml
+++ b/plugins/subtac/subtac_cases.ml
@@ -1,13 +1,13 @@
(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(************************************************************************)
(* 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: subtac_cases.ml 14003 2011-04-14 23:09:41Z letouzey $ *)
+(* $Id: subtac_cases.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Cases
open Util
diff --git a/plugins/subtac/subtac_cases.mli b/plugins/subtac/subtac_cases.mli
index a4df1257..bc2b2bb7 100644
--- a/plugins/subtac/subtac_cases.mli
+++ b/plugins/subtac/subtac_cases.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: subtac_cases.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: subtac_cases.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Util
diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 4927adbe..960bf162 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -1,13 +1,13 @@
(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(************************************************************************)
(* 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: subtac_classes.ml 13516 2010-10-07 19:09:38Z msozeau $ i*)
+(*i $Id: subtac_classes.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Pretyping
open Evd
@@ -160,7 +160,7 @@ let new_instance ?(global=false) ctx (instid, bk, cl) props ?(generalize=true) p
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
+ let term = Termops.it_mkLambda_or_LetIn (Option.get app) (ctx' @ ctx) in
term, termtype
| Inr def ->
let termtype = it_mkProd_or_LetIn cty ctx in
diff --git a/plugins/subtac/subtac_classes.mli b/plugins/subtac/subtac_classes.mli
index 57c7aa5b..73ca5581 100644
--- a/plugins/subtac/subtac_classes.mli
+++ b/plugins/subtac/subtac_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: subtac_classes.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: subtac_classes.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(*i*)
open Names
diff --git a/plugins/subtac/subtac_coercion.ml b/plugins/subtac/subtac_coercion.ml
index 17c7284c..bdebdf85 100644
--- a/plugins/subtac/subtac_coercion.ml
+++ b/plugins/subtac/subtac_coercion.ml
@@ -1,12 +1,12 @@
(* -*- 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 *)
(************************************************************************)
-(* $Id: subtac_coercion.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: subtac_coercion.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Names
diff --git a/plugins/subtac/subtac_pretyping.ml b/plugins/subtac/subtac_pretyping.ml
index 23323ab3..9de7ddf2 100644
--- a/plugins/subtac/subtac_pretyping.ml
+++ b/plugins/subtac/subtac_pretyping.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: subtac_pretyping.ml 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: subtac_pretyping.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Global
open Pp
diff --git a/plugins/subtac/subtac_pretyping_F.ml b/plugins/subtac/subtac_pretyping_F.ml
index 7fcd4267..4f4ae92e 100644
--- a/plugins/subtac/subtac_pretyping_F.ml
+++ b/plugins/subtac/subtac_pretyping_F.ml
@@ -1,13 +1,13 @@
(* -*- compile-command: "make -C ../.. plugins/subtac/subtac_plugin.cma" -*- *)
(************************************************************************)
(* 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: subtac_pretyping_F.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: subtac_pretyping_F.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pp
open Util
diff --git a/plugins/subtac/subtac_utils.ml b/plugins/subtac/subtac_utils.ml
index 689b110f..362c4ddc 100644
--- a/plugins/subtac/subtac_utils.ml
+++ b/plugins/subtac/subtac_utils.ml
@@ -23,6 +23,10 @@ let tactics_module = subtac_dir @ ["Tactics"]
let init_constant dir s () = gen_constant contrib_name dir s
let init_reference dir s () = gen_reference contrib_name dir s
+let safe_init_constant md name () =
+ check_required_library ("Coq"::md);
+ init_constant md name ()
+
let fixsub = init_constant fixsub_module "Fix_sub"
let ex_pi1 = init_constant utils_module "ex_pi1"
let ex_pi2 = init_constant utils_module "ex_pi2"
@@ -74,7 +78,7 @@ let eqdep_ind_ref = init_reference [ "Logic";"Eqdep"] "eq_dep"
let eqdep_intro_ref = init_reference [ "Logic";"Eqdep"] "eq_dep_intro"
let jmeq_ind =
- init_constant ["Logic";"JMeq"] "JMeq"
+ safe_init_constant ["Logic";"JMeq"] "JMeq"
let jmeq_rec =
init_constant ["Logic";"JMeq"] "JMeq_rec"
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 1e9a055f..7b92a92f 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.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: nat_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: nat_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
(* This file defines the printer for natural numbers in [nat] *)
diff --git a/plugins/syntax/numbers_syntax.ml b/plugins/syntax/numbers_syntax.ml
index 787577b2..a540a7d0 100644
--- a/plugins/syntax/numbers_syntax.ml
+++ b/plugins/syntax/numbers_syntax.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: numbers_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: numbers_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* digit-based syntax for int31, bigN bigZ and bigQ *)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index af1477f1..43e79c82 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.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: r_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: r_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Pp
open Util
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index 87f14a64..e6dcc35e 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.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: z_syntax.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: z_syntax.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Pcoq
open Pp
diff --git a/plugins/xml/acic.ml b/plugins/xml/acic.ml
index 653c2b7b..97287d18 100644
--- a/plugins/xml/acic.ml
+++ b/plugins/xml/acic.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/acic2Xml.ml4 b/plugins/xml/acic2Xml.ml4
index 97f7e2bd..631af9f0 100644
--- a/plugins/xml/acic2Xml.ml4
+++ b/plugins/xml/acic2Xml.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index da0a65ff..0b98acd2 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/doubleTypeInference.ml b/plugins/xml/doubleTypeInference.ml
index c8bb308f..d67c114e 100644
--- a/plugins/xml/doubleTypeInference.ml
+++ b/plugins/xml/doubleTypeInference.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/doubleTypeInference.mli b/plugins/xml/doubleTypeInference.mli
index 5c00bdc6..3858b906 100644
--- a/plugins/xml/doubleTypeInference.mli
+++ b/plugins/xml/doubleTypeInference.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/dumptree.ml4 b/plugins/xml/dumptree.ml4
index ce463b98..3cfc52b7 100644
--- a/plugins/xml/dumptree.ml4
+++ b/plugins/xml/dumptree.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 *)
diff --git a/plugins/xml/proof2aproof.ml b/plugins/xml/proof2aproof.ml
index 0c90babb..d871935b 100644
--- a/plugins/xml/proof2aproof.ml
+++ b/plugins/xml/proof2aproof.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4
index 6c57c400..21c86c79 100644
--- a/plugins/xml/proofTree2Xml.ml4
+++ b/plugins/xml/proofTree2Xml.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/unshare.ml b/plugins/xml/unshare.ml
index c854427d..344a1581 100644
--- a/plugins/xml/unshare.ml
+++ b/plugins/xml/unshare.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/unshare.mli b/plugins/xml/unshare.mli
index cace2de6..4b96b22e 100644
--- a/plugins/xml/unshare.mli
+++ b/plugins/xml/unshare.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/xml.ml4 b/plugins/xml/xml.ml4
index 8a4eb39a..2d73074b 100644
--- a/plugins/xml/xml.ml4
+++ b/plugins/xml/xml.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/xml.mli b/plugins/xml/xml.mli
index 2a9d1de4..ffaad957 100644
--- a/plugins/xml/xml.mli
+++ b/plugins/xml/xml.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
@@ -12,7 +12,7 @@
(* http://helm.cs.unibo.it *)
(************************************************************************)
-(*i $Id: xml.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: xml.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* Tokens for XML cdata, empty elements and not-empty elements *)
(* Usage: *)
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index e111a37f..7e7f890f 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
diff --git a/plugins/xml/xmlcommand.mli b/plugins/xml/xmlcommand.mli
index 476ad630..eadf3cfd 100644
--- a/plugins/xml/xmlcommand.mli
+++ b/plugins/xml/xmlcommand.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
@@ -12,7 +12,7 @@
(* http://helm.cs.unibo.it *)
(************************************************************************)
-(*i $Id: xmlcommand.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: xmlcommand.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
(* print_global qid fn *)
(* where qid is a long name denoting a definition/theorem or *)
diff --git a/plugins/xml/xmlentries.ml4 b/plugins/xml/xmlentries.ml4
index bf6c7388..f9d5bac0 100644
--- a/plugins/xml/xmlentries.ml4
+++ b/plugins/xml/xmlentries.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/ **************************************************************)
(* // * The HELM Project / The EU MoWGLI Project *)
(* * University of Bologna *)
@@ -14,7 +14,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: xmlentries.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: xmlentries.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util;;
open Vernacinterp;;