summaryrefslogtreecommitdiff
path: root/plugins/xml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
commit300293c119981054c95182a90c829058530a6b6f (patch)
treed7303613741c5796b58ced7db24ec7203327dbb2 /plugins/xml
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'plugins/xml')
-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
15 files changed, 18 insertions, 18 deletions
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;;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 05:36:59 +0000