diff options
| author | letouzey | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey | 2010-04-29 13:50:31 +0000 |
| commit | af93e4cf8b1a839d21499b3b9737bb8904edcae8 (patch) | |
| tree | b9a4f28e6f8106bcf19e017f64147f836f810c4b /pretyping | |
| parent | 0f61b02f84b41e1f019cd78824de28f18ff854aa (diff) | |
Remove the svn-specific $Id$ annotations
- Many of them were broken, some of them after Pierre B's rework
of mli for ocamldoc, but not only (many bad annotation, many files
with no svn property about Id, etc)
- Useless for those of us that work with git-svn (and a fortiori
in a forthcoming git-only setting)
- Even in svn, they seem to be of little interest
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12972 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
53 files changed, 0 insertions, 106 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index f68bf10c4b..4b565ddbd9 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Nameops diff --git a/pretyping/cases.mli b/pretyping/cases.mli index 188959f6a6..202a794abb 100644 --- a/pretyping/cases.mli +++ b/pretyping/cases.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Term diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml index 8c03d0df47..8a71827080 100644 --- a/pretyping/cbv.ml +++ b/pretyping/cbv.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Term diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli index 75017d5b45..50b4fda4a3 100644 --- a/pretyping/cbv.mli +++ b/pretyping/cbv.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Environ diff --git a/pretyping/classops.ml b/pretyping/classops.ml index 2379632582..5c30f05aae 100644 --- a/pretyping/classops.ml +++ b/pretyping/classops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Flags diff --git a/pretyping/classops.mli b/pretyping/classops.mli index 1830df3fbc..890aa005c2 100644 --- a/pretyping/classops.mli +++ b/pretyping/classops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Decl_kinds open Term diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 3607362a6d..f2975d21c0 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -5,8 +5,6 @@ (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli index 3ac83fc19d..a5ed740f96 100644 --- a/pretyping/coercion.mli +++ b/pretyping/coercion.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Evd open Names diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 6560f7b48d..9113efd559 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Univ diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli index 7b14c4fd2f..47a7beb539 100644 --- a/pretyping/detyping.mli +++ b/pretyping/detyping.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Term diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index b43e6e999c..4b76b77095 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli index 2e52fb12b9..8ea91d28ff 100644 --- a/pretyping/evarconv.mli +++ b/pretyping/evarconv.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Sign open Environ diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml index 6d37cf80f5..fbfb33cc37 100644 --- a/pretyping/evarutil.ml +++ b/pretyping/evarutil.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Names diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 3f66dc97e1..de50a87610 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Rawterm diff --git a/pretyping/evd.ml b/pretyping/evd.ml index 5b4a3f214d..61a0353dd9 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 2601d44f7e..ebf91b4f4b 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -7,8 +7,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Names open Term diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 1352b38300..1daae0236a 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* File initially created by Christine Paulin, 1996 *) (* This file builds various inductive schemes *) diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index 304b986a16..7f19c5d372 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Declarations diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3897b18e59..07447c5404 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Univ diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 6255a83d40..98a22fabd4 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Declarations diff --git a/pretyping/matching.ml b/pretyping/matching.ml index b94642c097..2c0285ed24 100644 --- a/pretyping/matching.ml +++ b/pretyping/matching.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (*i*) open Util open Names diff --git a/pretyping/matching.mli b/pretyping/matching.mli index 263ded3814..95314054e5 100644 --- a/pretyping/matching.mli +++ b/pretyping/matching.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Environ diff --git a/pretyping/namegen.ml b/pretyping/namegen.ml index 7d141faf1e..7f0b14f065 100644 --- a/pretyping/namegen.ml +++ b/pretyping/namegen.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (* Created from contents that was formerly in termops.ml and nameops.ml, Nov 2009 *) diff --git a/pretyping/namegen.mli b/pretyping/namegen.mli index e3ab7d03e3..889f8ec8cd 100644 --- a/pretyping/namegen.mli +++ b/pretyping/namegen.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id: namegen.mli 12549 2009-12-01 12:05:57Z herbelin {% $ %} *) - open Names open Term open Environ diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml index f9dec8f35f..48218f47f2 100644 --- a/pretyping/pattern.ml +++ b/pretyping/pattern.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Libnames diff --git a/pretyping/pattern.mli b/pretyping/pattern.mli index 33105c3128..d805730e97 100644 --- a/pretyping/pattern.mli +++ b/pretyping/pattern.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Names open Sign diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index 2f7a7c87cc..6adaee81c2 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Stdpp open Names diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index 9b6216a126..e6e01fc44e 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Pp open Util open Names diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 8654ca9479..92968cad90 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index f5601d6d65..eba26bafee 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Sign open Term diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index 16421b2a71..784e6b6e0f 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - (*i*) open Util open Names diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index ac4f0dec66..9e2d1f28cf 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Util open Names diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index d94da115a5..32433f6be6 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Pp open Names diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli index 954890d894..78b01eeab9 100755 --- a/pretyping/recordops.mli +++ b/pretyping/recordops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Nametab open Term diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index b741c9a413..dae6682439 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli index 84bd20135f..f3bfa1e5f4 100644 --- a/pretyping/reductionops.mli +++ b/pretyping/reductionops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Univ diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index 1e0649da6d..db0ee942a7 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Term open Inductive diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index 3c68f850b0..5b445ff9c0 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Evd diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index a103c49b61..6dbbff170b 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 84cff15b63..fdceadfbb3 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Term open Environ diff --git a/pretyping/term_dnet.ml b/pretyping/term_dnet.ml index 04e328cbdc..c7cfaed4b4 100644 --- a/pretyping/term_dnet.ml +++ b/pretyping/term_dnet.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id:$ *) - (*i*) open Util open Term diff --git a/pretyping/term_dnet.mli b/pretyping/term_dnet.mli index 7623fcd68d..3db55b1621 100644 --- a/pretyping/term_dnet.mli +++ b/pretyping/term_dnet.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(** {% $ %}Id:{% $ %} *) - open Term open Sign open Libnames diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 4de4bde2cb..1c0bf2fbcf 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 57b5bd5815..9f3884088f 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Util open Pp open Names diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml index 88d4a4d6b3..2a716ee6ad 100644 --- a/pretyping/typeclasses.ml +++ b/pretyping/typeclasses.ml @@ -7,8 +7,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Names open Libnames diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli index c816f2e9c9..dc1c5f5569 100644 --- a/pretyping/typeclasses.mli +++ b/pretyping/typeclasses.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Libnames open Decl_kinds diff --git a/pretyping/typeclasses_errors.ml b/pretyping/typeclasses_errors.ml index 1de8b7a5fb..869a7845d1 100644 --- a/pretyping/typeclasses_errors.ml +++ b/pretyping/typeclasses_errors.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - (*i*) open Names open Decl_kinds diff --git a/pretyping/typeclasses_errors.mli b/pretyping/typeclasses_errors.mli index 24a19a0e37..43b3495150 100644 --- a/pretyping/typeclasses_errors.mli +++ b/pretyping/typeclasses_errors.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Names open Decl_kinds open Term diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 831787a06e..8670b95f9d 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Util open Names open Term diff --git a/pretyping/typing.mli b/pretyping/typing.mli index c20fd9453a..90f823b8e1 100644 --- a/pretyping/typing.mli +++ b/pretyping/typing.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Environ open Evd diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 35543ce24a..7ae05a85f0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id$ *) - open Pp open Util open Names diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 13042180a8..8829d8989d 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -6,8 +6,6 @@ * GNU Lesser General Public License Version 2.1 ***********************************************************************) -(*i $Id$ i*) - open Term open Environ open Evd diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c894d2b519..7e41e2125c 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -6,8 +6,6 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id$ i*) - open Names open Declarations open Term |