diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-04-29 13:50:31 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 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 f68bf10c4..4b565ddbd 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 188959f6a..202a794ab 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 8c03d0df4..8a7182708 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 75017d5b4..50b4fda4a 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 237963258..5c30f05aa 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 1830df3fb..890aa005c 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 3607362a6..f2975d21c 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 3ac83fc19..a5ed740f9 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 6560f7b48..9113efd55 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 7b14c4fd2..47a7beb53 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 b43e6e999..4b76b7709 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 2e52fb12b..8ea91d28f 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 6d37cf80f..fbfb33cc3 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 3f66dc97e..de50a8761 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 5b4a3f214..61a0353dd 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 2601d44f7..ebf91b4f4 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 1352b3830..1daae0236 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 304b986a1..7f19c5d37 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 3897b18e5..07447c540 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 6255a83d4..98a22fabd 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 b94642c09..2c0285ed2 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 263ded381..95314054e 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 7d141faf1..7f0b14f06 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 e3ab7d03e..889f8ec8c 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 f9dec8f35..48218f47f 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 33105c312..d805730e9 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 2f7a7c87c..6adaee81c 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 9b6216a12..e6e01fc44 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 8654ca947..92968cad9 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 f5601d6d6..eba26bafe 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 16421b2a7..784e6b6e0 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 ac4f0dec6..9e2d1f28c 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 d94da115a..32433f6be 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 954890d89..78b01eeab 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 b741c9a41..dae668243 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 84bd20135..f3bfa1e5f 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 1e0649da6..db0ee942a 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 3c68f850b..5b445ff9c 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 a103c49b6..6dbbff170 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 84cff15b6..fdceadfbb 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 04e328cbd..c7cfaed4b 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 7623fcd68..3db55b162 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 4de4bde2c..1c0bf2fbc 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 57b5bd581..9f3884088 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 88d4a4d6b..2a716ee6a 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 c816f2e9c..dc1c5f556 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 1de8b7a5f..869a7845d 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 24a19a0e3..43b349515 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 831787a06..8670b95f9 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 c20fd9453..90f823b8e 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 35543ce24..7ae05a85f 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 13042180a..8829d8989 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 c894d2b51..7e41e2125 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 |