aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-21 16:45:23 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2016-01-21 16:45:23 +0100
commitbe0eca32fae93ed4793c2f839bb9e725b6a963d1 (patch)
treec2c5dce5ce24f5a2a8cade9e69410599c00e2b55 /toplevel
parent9c2662eecc398f38be3b6280a8f760cc439bc31c (diff)
parent5e23fb90b39dfa014ae5c4fb46eb713cca09dbff (diff)
Merge branch 'v8.5'
Diffstat (limited to 'toplevel')
-rw-r--r--toplevel/assumptions.ml2
-rw-r--r--toplevel/assumptions.mli2
-rw-r--r--toplevel/auto_ind_decl.ml2
-rw-r--r--toplevel/auto_ind_decl.mli2
-rw-r--r--toplevel/cerrors.ml2
-rw-r--r--toplevel/cerrors.mli2
-rw-r--r--toplevel/class.ml2
-rw-r--r--toplevel/class.mli2
-rw-r--r--toplevel/classes.ml2
-rw-r--r--toplevel/classes.mli2
-rw-r--r--toplevel/command.ml2
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/coqinit.ml2
-rw-r--r--toplevel/coqinit.mli2
-rw-r--r--toplevel/coqloop.ml2
-rw-r--r--toplevel/coqloop.mli2
-rw-r--r--toplevel/coqtop.ml4
-rw-r--r--toplevel/coqtop.mli2
-rw-r--r--toplevel/discharge.ml2
-rw-r--r--toplevel/discharge.mli2
-rw-r--r--toplevel/g_obligations.ml42
-rw-r--r--toplevel/himsg.ml2
-rw-r--r--toplevel/himsg.mli2
-rw-r--r--toplevel/ind_tables.ml2
-rw-r--r--toplevel/ind_tables.mli2
-rw-r--r--toplevel/indschemes.ml2
-rw-r--r--toplevel/indschemes.mli2
-rw-r--r--toplevel/locality.ml2
-rw-r--r--toplevel/locality.mli2
-rw-r--r--toplevel/metasyntax.ml2
-rw-r--r--toplevel/metasyntax.mli2
-rw-r--r--toplevel/mltop.ml2
-rw-r--r--toplevel/mltop.mli2
-rw-r--r--toplevel/obligations.mli2
-rw-r--r--toplevel/record.ml2
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/search.ml2
-rw-r--r--toplevel/search.mli2
-rw-r--r--toplevel/usage.ml5
-rw-r--r--toplevel/usage.mli2
-rw-r--r--toplevel/vernac.ml8
-rw-r--r--toplevel/vernac.mli6
-rw-r--r--toplevel/vernacentries.ml2
-rw-r--r--toplevel/vernacentries.mli2
-rw-r--r--toplevel/vernacinterp.ml2
-rw-r--r--toplevel/vernacinterp.mli2
46 files changed, 60 insertions, 47 deletions
diff --git a/toplevel/assumptions.ml b/toplevel/assumptions.ml
index 470485438..cddc55515 100644
--- a/toplevel/assumptions.ml
+++ b/toplevel/assumptions.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/assumptions.mli b/toplevel/assumptions.mli
index 21039f571..072675783 100644
--- a/toplevel/assumptions.mli
+++ b/toplevel/assumptions.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 2f206bfc8..f0c7a3961 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/auto_ind_decl.mli b/toplevel/auto_ind_decl.mli
index 20a3d5d74..b6c66a1e8 100644
--- a/toplevel/auto_ind_decl.mli
+++ b/toplevel/auto_ind_decl.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index accba3121..600683d35 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 729686f32..68c46010b 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 28a39b570..a9c53b4d4 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/class.mli b/toplevel/class.mli
index bd6c7a6d1..5f9ae28f6 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 86b471232..936343628 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index 80ed24629..8dcfabae4 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 500769aca..4adb66bc9 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8e2d9c6fc..b97cb487d 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index e089b7ecc..b81c8da71 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index c019cc1ce..4ff87628c 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml
index caaf8054b..063ed8964 100644
--- a/toplevel/coqloop.ml
+++ b/toplevel/coqloop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/coqloop.mli b/toplevel/coqloop.mli
index 8ed661e67..00554da30 100644
--- a/toplevel/coqloop.mli
+++ b/toplevel/coqloop.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index bd0a79caf..8f56cddfa 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -543,6 +543,7 @@ let parse_args arglist =
|"-v"|"--version" -> Usage.version (exitcode ())
|"-verbose-compat-notations" -> verb_compat_ntn := true
|"-where" -> print_where := true
+ |"-xml" -> Flags.xml_export := true
(* Deprecated options *)
|"-byte" -> warning "option -byte deprecated, call with .byte suffix"
@@ -558,7 +559,6 @@ let parse_args arglist =
|"-force-load-proofs" -> warning "Obsolete option \"-force-load-proofs\"."
|"-unsafe" -> warning "Obsolete option \"-unsafe\"."; ignore (next ())
|"-quality" -> warning "Obsolete option \"-quality\"."
- |"-xml" -> warning "Obsolete option \"-xml\"."
(* Unknown option *)
| s -> extras := s :: !extras
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 670447452..c9d1ba45d 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 9416b7e7a..61a6e1094 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 2984a0be8..18d1b6776 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/g_obligations.ml4 b/toplevel/g_obligations.ml4
index 24661e124..d620febbc 100644
--- a/toplevel/g_obligations.ml4
+++ b/toplevel/g_obligations.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 3ac537297..819c290af 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index 3d5442bb1..3ef98380b 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml
index dde801a7f..35717ed61 100644
--- a/toplevel/ind_tables.ml
+++ b/toplevel/ind_tables.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/ind_tables.mli b/toplevel/ind_tables.mli
index abd951c31..20f30d6d1 100644
--- a/toplevel/ind_tables.mli
+++ b/toplevel/ind_tables.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 00197bd66..c4ac0e411 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/indschemes.mli b/toplevel/indschemes.mli
index 987461078..e5d79fd51 100644
--- a/toplevel/indschemes.mli
+++ b/toplevel/indschemes.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/locality.ml b/toplevel/locality.ml
index 1145a20bb..ef789aa5c 100644
--- a/toplevel/locality.ml
+++ b/toplevel/locality.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/locality.mli b/toplevel/locality.mli
index c395fe921..2ec392eef 100644
--- a/toplevel/locality.mli
+++ b/toplevel/locality.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml
index 9a27ae7df..6534c39a7 100644
--- a/toplevel/metasyntax.ml
+++ b/toplevel/metasyntax.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index f7049999e..826886f67 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index fa5ed7bbd..d0fa7a80c 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 4f3f4ddde..5d0546824 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/obligations.mli b/toplevel/obligations.mli
index 2e3aa6005..b2320a578 100644
--- a/toplevel/obligations.mli
+++ b/toplevel/obligations.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 408d3fa5f..7ae203034 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index f68adcec8..26eb3378b 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/search.ml b/toplevel/search.ml
index 9c32bddad..89e0eb88a 100644
--- a/toplevel/search.ml
+++ b/toplevel/search.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/search.mli b/toplevel/search.mli
index f69489c3d..78b0c45c0 100644
--- a/toplevel/search.mli
+++ b/toplevel/search.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/usage.ml b/toplevel/usage.ml
index 292136406..f855c096e 100644
--- a/toplevel/usage.ml
+++ b/toplevel/usage.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -73,6 +73,9 @@ let print_usage_channel co command =
\n -impredicative-set set sort Set impredicative\
\n -indices-matter levels of indices (and nonuniform parameters) contribute to the level of inductives\
\n -type-in-type disable universe consistency checking\
+\n -xml export XML files either to the hierarchy rooted in\
+\n the directory $COQ_XML_LIBRARY_ROOT (if set) or to\
+\n stdout (if unset)\
\n -time display the time taken by each command\
\n -m, --memory display total heap size at program exit\
\n (use environment variable\
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index ed0cd477c..3ce9e93ee 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml
index 7b80becda..89bc31d0a 100644
--- a/toplevel/vernac.ml
+++ b/toplevel/vernac.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -276,6 +276,10 @@ let checknav loc ast =
let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast
+(* XML output hooks *)
+let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore ()
+let (f_xml_end_library, xml_end_library) = Hook.make ~default:ignore ()
+
(* Load a vernac file. Errors are annotated with file and location *)
let load_vernac verb file =
chan_beautify :=
@@ -310,6 +314,7 @@ let compile verbosely f =
Aux_file.start_aux_file_for long_f_dot_v;
Dumpglob.start_dump_glob long_f_dot_v;
Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n");
+ if !Flags.xml_export then Hook.get f_xml_start_library ();
let wall_clock1 = Unix.gettimeofday () in
let _ = load_vernac verbosely long_f_dot_v in
Stm.join ();
@@ -319,6 +324,7 @@ let compile verbosely f =
Aux_file.record_in_aux_at Loc.ghost "vo_compile_time"
(Printf.sprintf "%.3f" (wall_clock2 -. wall_clock1));
Aux_file.stop_aux_file ();
+ if !Flags.xml_export then Hook.get f_xml_end_library ();
Dumpglob.end_dump_glob ()
| BuildVio ->
let long_f_dot_v = ensure_v f in
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index affc21713..008d7a31a 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -23,6 +23,10 @@ val just_parsing : bool ref
val eval_expr : Loc.t * Vernacexpr.vernac_expr -> unit
+(** Set XML hooks *)
+val xml_start_library : (unit -> unit) Hook.t
+val xml_end_library : (unit -> unit) Hook.t
+
(** Load a vernac file, verbosely or not. Errors are annotated with file
and location *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 55e57ec69..0f81943e2 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index c6d87596d..451ccdb4d 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/vernacinterp.ml b/toplevel/vernacinterp.ml
index d3e48f756..7fbd2b119 100644
--- a/toplevel/vernacinterp.ml
+++ b/toplevel/vernacinterp.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 028206546..5149b5416 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)