diff options
Diffstat (limited to 'proofs')
-rw-r--r-- | proofs/clenvtac.ml | 2 | ||||
-rw-r--r-- | proofs/clenvtac.mli | 2 | ||||
-rw-r--r-- | proofs/decl_expr.mli | 2 | ||||
-rw-r--r-- | proofs/decl_mode.ml | 2 | ||||
-rw-r--r-- | proofs/decl_mode.mli | 2 | ||||
-rw-r--r-- | proofs/evar_refiner.ml | 2 | ||||
-rw-r--r-- | proofs/evar_refiner.mli | 2 | ||||
-rw-r--r-- | proofs/logic.ml | 2 | ||||
-rw-r--r-- | proofs/logic.mli | 2 | ||||
-rw-r--r-- | proofs/pfedit.ml | 2 | ||||
-rw-r--r-- | proofs/pfedit.mli | 2 | ||||
-rw-r--r-- | proofs/proof_trees.ml | 2 | ||||
-rw-r--r-- | proofs/proof_trees.mli | 2 | ||||
-rw-r--r-- | proofs/proof_type.ml | 2 | ||||
-rw-r--r-- | proofs/proof_type.mli | 2 | ||||
-rw-r--r-- | proofs/redexpr.ml | 2 | ||||
-rw-r--r-- | proofs/redexpr.mli | 2 | ||||
-rw-r--r-- | proofs/refiner.ml | 2 | ||||
-rw-r--r-- | proofs/refiner.mli | 2 | ||||
-rw-r--r-- | proofs/tacexpr.ml | 2 | ||||
-rw-r--r-- | proofs/tacmach.ml | 2 | ||||
-rw-r--r-- | proofs/tacmach.mli | 2 | ||||
-rw-r--r-- | proofs/tactic_debug.ml | 2 | ||||
-rw-r--r-- | proofs/tactic_debug.mli | 2 |
24 files changed, 24 insertions, 24 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 9bc818e8..de2ba7c9 100644 --- a/proofs/clenvtac.ml +++ b/proofs/clenvtac.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/proofs/clenvtac.mli b/proofs/clenvtac.mli index 96fb262a..72b812ce 100644 --- a/proofs/clenvtac.mli +++ b/proofs/clenvtac.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/proofs/decl_expr.mli b/proofs/decl_expr.mli index bf5fa2e9..91f0a9ff 100644 --- a/proofs/decl_expr.mli +++ b/proofs/decl_expr.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/proofs/decl_mode.ml b/proofs/decl_mode.ml index 8be5f355..d28d9a0d 100644 --- a/proofs/decl_mode.ml +++ b/proofs/decl_mode.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/proofs/decl_mode.mli b/proofs/decl_mode.mli index 1ecd4d3a..b6e77b43 100644 --- a/proofs/decl_mode.mli +++ b/proofs/decl_mode.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/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index e4fab3f2..a5a0cde4 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.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/proofs/evar_refiner.mli b/proofs/evar_refiner.mli index 30e702a0..e4303f42 100644 --- a/proofs/evar_refiner.mli +++ b/proofs/evar_refiner.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/proofs/logic.ml b/proofs/logic.ml index 9cab6a05..83dc497c 100644 --- a/proofs/logic.ml +++ b/proofs/logic.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/proofs/logic.mli b/proofs/logic.mli index 0d56da38..c7cf6472 100644 --- a/proofs/logic.mli +++ b/proofs/logic.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/proofs/pfedit.ml b/proofs/pfedit.ml index f3658ad4..3adfd522 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.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/proofs/pfedit.mli b/proofs/pfedit.mli index acb85247..b5003425 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.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/proofs/proof_trees.ml b/proofs/proof_trees.ml index a5bd073a..b352fdc8 100644 --- a/proofs/proof_trees.ml +++ b/proofs/proof_trees.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/proofs/proof_trees.mli b/proofs/proof_trees.mli index 6d1fc143..477c3162 100644 --- a/proofs/proof_trees.mli +++ b/proofs/proof_trees.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/proofs/proof_type.ml b/proofs/proof_type.ml index 1daddde9..f7c937bd 100644 --- a/proofs/proof_type.ml +++ b/proofs/proof_type.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/proofs/proof_type.mli b/proofs/proof_type.mli index c4a48c3c..c6f0658b 100644 --- a/proofs/proof_type.mli +++ b/proofs/proof_type.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/proofs/redexpr.ml b/proofs/redexpr.ml index b0a01caa..f7d83c0a 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.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/proofs/redexpr.mli b/proofs/redexpr.mli index 03d97ce3..93c34d86 100644 --- a/proofs/redexpr.mli +++ b/proofs/redexpr.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/proofs/refiner.ml b/proofs/refiner.ml index a320b67c..e0ed7861 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.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/proofs/refiner.mli b/proofs/refiner.mli index e853c12b..2b213c3f 100644 --- a/proofs/refiner.mli +++ b/proofs/refiner.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/proofs/tacexpr.ml b/proofs/tacexpr.ml index b56e5184..8761bfae 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.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/proofs/tacmach.ml b/proofs/tacmach.ml index 9e35abfc..60e79c19 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.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/proofs/tacmach.mli b/proofs/tacmach.mli index a808ca41..489786ef 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.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/proofs/tactic_debug.ml b/proofs/tactic_debug.ml index ea8ab5b6..6455420c 100644 --- a/proofs/tactic_debug.ml +++ b/proofs/tactic_debug.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/proofs/tactic_debug.mli b/proofs/tactic_debug.mli index 0a5e6087..8a6a22c6 100644 --- a/proofs/tactic_debug.mli +++ b/proofs/tactic_debug.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 *) |