summaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2010-07-24 20:01:08 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2010-07-24 20:01:08 +0200
commitb9f47391f7f259c24119d1de0a87839e2cc5e80c (patch)
tree26dd3d5de63f420384fd84196d3a144af01f6084 /tools
parent5b7eafd0f00a16d78f99a27f5c7d5a0de77dc7e6 (diff)
Imported Upstream snapshot 8.3~beta0+13323
Diffstat (limited to 'tools')
-rw-r--r--tools/coq-db.el15
-rw-r--r--tools/coq_makefile.ml44
-rw-r--r--tools/coq_tex.ml42
-rw-r--r--tools/coqdep.ml2
-rw-r--r--tools/coqdep_boot.ml2
-rw-r--r--tools/coqdep_common.ml2
-rw-r--r--[-rwxr-xr-x]tools/coqdep_lexer.mll2
-rw-r--r--tools/coqdoc/alpha.ml2
-rw-r--r--tools/coqdoc/alpha.mli2
-rw-r--r--tools/coqdoc/cdglobals.ml2
-rw-r--r--tools/coqdoc/cpretty.mli2
-rw-r--r--tools/coqdoc/cpretty.mll2
-rw-r--r--tools/coqdoc/index.ml2
-rw-r--r--tools/coqdoc/index.mli2
-rw-r--r--tools/coqdoc/main.ml2
-rw-r--r--tools/coqdoc/output.ml2
-rw-r--r--tools/coqdoc/output.mli2
-rw-r--r--tools/coqdoc/tokens.ml2
-rw-r--r--tools/coqdoc/tokens.mli2
-rw-r--r--tools/coqwc.mll2
-rw-r--r--tools/gallina.ml2
-rw-r--r--tools/gallina_lexer.mll2
22 files changed, 29 insertions, 30 deletions
diff --git a/tools/coq-db.el b/tools/coq-db.el
index 078c2bb6..5081b10b 100644
--- a/tools/coq-db.el
+++ b/tools/coq-db.el
@@ -216,19 +216,18 @@ See `coq-syntax-db' for DB structure."
"Not documented."
(nth 3 l)) ; fourth argument is nil --> state preserving command
+(defconst coq-solve-tactics-face 'coq-solve-tactics-face
+ "Expression that evaluates to a face.
+Required so that 'proof-solve-tactics-face is a proper facename")
+
;;A new face for tactics which fail when they don't kill the current goal
-(defface coq-solve-tactics-face
- (proof-face-specs
- (:foreground "red" t) ; pour les fonds clairs
- (:foreground "red" t) ; pour les fond foncés
- ()) ; pour le noir et blanc
+(defface coq-solve-tactics-face
+ '((t (:background "red")))
"Face for names of closing tactics in proof scripts."
:group 'proof-faces)
-(defconst coq-solve-tactics-face 'coq-solve-tactics-face
- "Expression that evaluates to a face.
-Required so that 'proof-solve-tactics-face is a proper facename")
+
diff --git a/tools/coq_makefile.ml4 b/tools/coq_makefile.ml4
index 338aba99..6be4d188 100644
--- a/tools/coq_makefile.ml4
+++ b/tools/coq_makefile.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -507,7 +507,7 @@ let banner () =
print (Printf.sprintf
"#############################################################################
## v # The Coq Proof Assistant ##
-## <O___,, # CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud ##
+## <O___,, # INRIA - CNRS - LIX - LRI - PPS ##
## \\VV/ # ##
## // # Makefile automagically generated by coq_makefile V%s ##
#############################################################################
diff --git a/tools/coq_tex.ml4 b/tools/coq_tex.ml4
index c46a187c..f2f7ebc4 100644
--- a/tools/coq_tex.ml4
+++ b/tools/coq_tex.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdep.ml b/tools/coqdep.ml
index fe930a1d..08bd8ba0 100644
--- a/tools/coqdep.ml
+++ b/tools/coqdep.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml
index b7f6ec25..7de7d395 100644
--- a/tools/coqdep_boot.ml
+++ b/tools/coqdep_boot.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdep_common.ml b/tools/coqdep_common.ml
index b71a47d0..c4e8b23c 100644
--- a/tools/coqdep_common.ml
+++ b/tools/coqdep_common.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdep_lexer.mll b/tools/coqdep_lexer.mll
index 89eeed54..a0880d7f 100755..100644
--- a/tools/coqdep_lexer.mll
+++ b/tools/coqdep_lexer.mll
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/alpha.ml b/tools/coqdoc/alpha.ml
index d25034f2..34b27253 100644
--- a/tools/coqdoc/alpha.ml
+++ b/tools/coqdoc/alpha.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/alpha.mli b/tools/coqdoc/alpha.mli
index 922a10d6..cecfe1a6 100644
--- a/tools/coqdoc/alpha.mli
+++ b/tools/coqdoc/alpha.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/cdglobals.ml b/tools/coqdoc/cdglobals.ml
index b2e23657..63ea264b 100644
--- a/tools/coqdoc/cdglobals.ml
+++ b/tools/coqdoc/cdglobals.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/cpretty.mli b/tools/coqdoc/cpretty.mli
index 213c76aa..76d85455 100644
--- a/tools/coqdoc/cpretty.mli
+++ b/tools/coqdoc/cpretty.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index be8bc85d..9367faed 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -1,7 +1,7 @@
(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/index.ml b/tools/coqdoc/index.ml
index 889e5d6f..95950fb0 100644
--- a/tools/coqdoc/index.ml
+++ b/tools/coqdoc/index.ml
@@ -1,7 +1,7 @@
(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/index.mli b/tools/coqdoc/index.mli
index 517ec97a..bf1d6568 100644
--- a/tools/coqdoc/index.mli
+++ b/tools/coqdoc/index.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/main.ml b/tools/coqdoc/main.ml
index 67c63865..6b750556 100644
--- a/tools/coqdoc/main.ml
+++ b/tools/coqdoc/main.ml
@@ -1,7 +1,7 @@
(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 93e1f843..dda704fa 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -1,7 +1,7 @@
(* -*- compile-command: "make -C ../.. bin/coqdoc" -*- *)
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/output.mli b/tools/coqdoc/output.mli
index d836f6b3..60408689 100644
--- a/tools/coqdoc/output.mli
+++ b/tools/coqdoc/output.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/tokens.ml b/tools/coqdoc/tokens.ml
index c2a47308..a228797e 100644
--- a/tools/coqdoc/tokens.ml
+++ b/tools/coqdoc/tokens.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqdoc/tokens.mli b/tools/coqdoc/tokens.mli
index a85e75c4..6adc2d8c 100644
--- a/tools/coqdoc/tokens.mli
+++ b/tools/coqdoc/tokens.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index f3646a8a..173ed2ed 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/gallina.ml b/tools/gallina.ml
index 8ba9ae10..fe9766ec 100644
--- a/tools/gallina.ml
+++ b/tools/gallina.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/tools/gallina_lexer.mll b/tools/gallina_lexer.mll
index 6d35d839..9622beee 100644
--- a/tools/gallina_lexer.mll
+++ b/tools/gallina_lexer.mll
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-04-28 07:07:57 +0000