diff options
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 |