aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.depend6
-rw-r--r--PROBLEMES10
-rw-r--r--config/coq_config.mli2
-rw-r--r--contrib/xml/xml.mli2
-rw-r--r--contrib/xml/xmlcommand.mli2
-rw-r--r--kernel/closure.mli2
-rw-r--r--kernel/declarations.mli2
-rw-r--r--kernel/environ.mli2
-rw-r--r--kernel/evd.mli2
-rw-r--r--kernel/indtypes.mli2
-rw-r--r--kernel/inductive.mli2
-rw-r--r--kernel/instantiate.mli2
-rw-r--r--kernel/names.mli2
-rw-r--r--kernel/reduction.mli2
-rw-r--r--kernel/safe_typing.ml3
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/sign.mli2
-rw-r--r--kernel/term.ml6
-rw-r--r--kernel/term.mli2
-rw-r--r--kernel/type_errors.mli2
-rw-r--r--kernel/typeops.mli2
-rw-r--r--kernel/univ.mli2
-rw-r--r--lib/bij.mli2
-rw-r--r--lib/bstack.mli2
-rw-r--r--lib/dyn.mli2
-rw-r--r--lib/edit.mli2
-rw-r--r--lib/gmap.mli2
-rw-r--r--lib/gmapl.mli2
-rw-r--r--lib/gset.mli2
-rw-r--r--lib/hashcons.mli2
-rw-r--r--lib/options.mli2
-rw-r--r--lib/pp.mli2
-rw-r--r--lib/pp_control.mli2
-rw-r--r--lib/profile.mli2
-rw-r--r--lib/stamps.mli2
-rw-r--r--lib/system.mli2
-rw-r--r--lib/tlm.mli2
-rw-r--r--lib/util.mli2
-rw-r--r--library/declare.ml10
-rw-r--r--library/declare.mli2
-rw-r--r--library/global.mli2
-rw-r--r--library/goptions.mli2
-rw-r--r--library/impargs.mli2
-rw-r--r--library/indrec.mli2
-rw-r--r--library/lib.mli2
-rw-r--r--library/libobject.mli2
-rw-r--r--library/library.mli2
-rwxr-xr-xlibrary/nametab.mli2
-rw-r--r--library/states.ml3
-rw-r--r--library/states.mli2
-rw-r--r--library/summary.mli2
-rwxr-xr-xparsing/ast.mli2
-rw-r--r--parsing/astterm.mli2
-rw-r--r--parsing/coqast.mli2
-rw-r--r--parsing/egrammar.mli2
-rw-r--r--parsing/esyntax.mli2
-rw-r--r--parsing/extend.mli2
-rw-r--r--parsing/g_minicoq.mli2
-rw-r--r--parsing/g_natsyntax.mli2
-rw-r--r--parsing/g_zsyntax.mli2
-rw-r--r--parsing/lexer.mli2
-rw-r--r--parsing/pattern.mli2
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/pretty.mli2
-rw-r--r--parsing/printer.mli2
-rw-r--r--parsing/search.ml4
-rw-r--r--parsing/search.mli2
-rw-r--r--parsing/termast.mli2
-rw-r--r--pretyping/cases.mli2
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/coercion.mli2
-rw-r--r--pretyping/detyping.mli2
-rw-r--r--pretyping/evarconv.mli2
-rw-r--r--pretyping/evarutil.mli2
-rw-r--r--pretyping/multcase.mli2
-rw-r--r--pretyping/pretype_errors.mli2
-rw-r--r--pretyping/pretyping.mli2
-rw-r--r--pretyping/rawterm.mli2
-rwxr-xr-xpretyping/recordops.mli2
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/syntax_def.mli2
-rw-r--r--pretyping/tacred.mli2
-rw-r--r--pretyping/typing.mli2
-rw-r--r--proofs/clenv.mli2
-rw-r--r--proofs/evar_refiner.mli2
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof_trees.mli2
-rw-r--r--proofs/proof_type.mli2
-rw-r--r--proofs/refiner.mli2
-rw-r--r--proofs/stock.mli2
-rw-r--r--proofs/tacinterp.mli2
-rw-r--r--proofs/tacmach.mli2
-rw-r--r--proofs/tactic_debug.mli3
-rw-r--r--tactics/Inv.v4
-rw-r--r--tactics/auto.mli2
-rw-r--r--tactics/autorewrite.mli3
-rw-r--r--tactics/btermdn.mli2
-rw-r--r--tactics/dhyp.mli2
-rw-r--r--tactics/dn.mli2
-rw-r--r--tactics/elim.mli2
-rw-r--r--tactics/equality.mli2
-rw-r--r--tactics/hiddentac.mli2
-rw-r--r--tactics/hipattern.mli2
-rw-r--r--tactics/inv.mli2
-rw-r--r--tactics/leminv.ml6
-rw-r--r--tactics/nbtermdn.mli2
-rw-r--r--tactics/refine.mli2
-rw-r--r--tactics/tacentries.mli2
-rw-r--r--tactics/tacticals.mli2
-rw-r--r--tactics/tactics.mli2
-rw-r--r--tactics/termdn.mli2
-rw-r--r--tactics/wcclausenv.mli2
-rw-r--r--toplevel/class.mli2
-rw-r--r--toplevel/command.mli2
-rw-r--r--toplevel/coqinit.mli2
-rw-r--r--toplevel/coqtop.mli2
-rw-r--r--toplevel/discharge.mli2
-rw-r--r--toplevel/errors.mli2
-rw-r--r--toplevel/fhimsg.mli2
-rw-r--r--toplevel/himsg.mli2
-rw-r--r--toplevel/line_oriented_parser.mli2
-rw-r--r--toplevel/metasyntax.mli2
-rw-r--r--toplevel/mltop.mli2
-rw-r--r--toplevel/protectedtoplevel.mli2
-rw-r--r--toplevel/record.mli2
-rw-r--r--toplevel/searchisos.mli2
-rw-r--r--toplevel/toplevel.mli2
-rw-r--r--toplevel/usage.mli2
-rw-r--r--toplevel/vernac.mli2
-rw-r--r--toplevel/vernacentries.ml10
-rw-r--r--toplevel/vernacentries.mli2
-rw-r--r--toplevel/vernacinterp.mli2
133 files changed, 168 insertions, 142 deletions
diff --git a/.depend b/.depend
index 83fe598fc..375065ff5 100644
--- a/.depend
+++ b/.depend
@@ -960,6 +960,12 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx \
kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
kernel/term.cmx lib/util.cmx tactics/tactics.cmi
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+ proofs/tacmach.cmi tactics/tacticals.cmi
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+ kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+ proofs/tacmach.cmx tactics/tacticals.cmx
tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi parsing/pattern.cmi \
pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi
tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx parsing/pattern.cmx \
diff --git a/PROBLEMES b/PROBLEMES
index fca3fc36a..5a55d23b9 100644
--- a/PROBLEMES
+++ b/PROBLEMES
@@ -39,18 +39,14 @@ CONTRIBS
BellLabs/lazyPCF : OK
Bordeaux/TREES :
-File "./ABR.v", line 131, characters 0-88
-Anomaly: Unrecognizable ast node of vernac arg:
- (COMMAND (PROP {Null})). Please report.
-
-Derive Inversion_clear HAS_INV with
- (n,p:nat)(t1,t2:bintree)(has (bin n t1 t2) p).
-
Bordeaux/Additions :
echecs sur Realizer
Bordeaux/GROUPS : OK
+Bordeaux/EXCEPTIONS :
+ Hints Unfold n'unfold plus les Local => échec d'Auto
+
Dyade/Otway-Rees : OK
Dyade/BDD : Require Rocq/GRAPHS
diff --git a/config/coq_config.mli b/config/coq_config.mli
index d896d6175..d4c18da8b 100644
--- a/config/coq_config.mli
+++ b/config/coq_config.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
val local : bool (* local use (no installation) *)
diff --git a/contrib/xml/xml.mli b/contrib/xml/xml.mli
index 6f1dd08b3..0510d978d 100644
--- a/contrib/xml/xml.mli
+++ b/contrib/xml/xml.mli
@@ -11,6 +11,8 @@
(* *)
(******************************************************************************)
+(*i $Id$ i*)
+
(* Tokens for XML cdata, empty elements and not-empty elements *)
(* Usage: *)
(* Str cdata *)
diff --git a/contrib/xml/xmlcommand.mli b/contrib/xml/xmlcommand.mli
index 84c71f0d7..827cb34f6 100644
--- a/contrib/xml/xmlcommand.mli
+++ b/contrib/xml/xmlcommand.mli
@@ -11,6 +11,8 @@
(* *)
(******************************************************************************)
+(*i $Id$ i*)
+
(* print id dest *)
(* where id is the identifier (name) of a definition/theorem or of an *)
(* inductive definition *)
diff --git a/kernel/closure.mli b/kernel/closure.mli
index b546942e1..c38c6aaa0 100644
--- a/kernel/closure.mli
+++ b/kernel/closure.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 3e7d8a9bd..0cc927c8c 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 14209cd72..eb6a45480 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/evd.mli b/kernel/evd.mli
index 6ab60e295..2353b6789 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 00e108460..71041c279 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 054a7d3fe..547979fde 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index 9f790e3ca..a80dcc435 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/names.mli b/kernel/names.mli
index cca174463..afdcd3a54 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 10b4edc43..7828ff940 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 642673a8a..c0e700a13 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -312,6 +312,7 @@ let add_discharged_constant sp r env =
| None ->
add_parameter sp typ env
| Some c ->
+ (* let c = hcons1_constr c in *)
let (jtyp,cst) = safe_infer env typ in
let env' = add_constraints cst env in
let ids =
@@ -319,7 +320,7 @@ let add_discharged_constant sp r env =
(global_vars_set (body_of_type jtyp.uj_val))
in
let cb = { const_kind = kind_of_path sp;
- const_body = body;
+ const_body = Some c;
const_type = assumption_of_judgment env' Evd.empty jtyp;
const_hyps = keep_hyps ids (named_context env);
const_constraints = cst;
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 011d0e414..7f50c7104 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/kernel/sign.mli b/kernel/sign.mli
index 38d058042..5c93bccbf 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/term.ml b/kernel/term.ml
index ff96a8e15..7a3c7e053 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -1668,10 +1668,10 @@ let hcons_constr (hspcci,hspfw,hname,hident,hstr) =
let htcci = Hashcons.simple_hcons Htype.f (hcci,hsortscci) in
(hcci,hfw,htcci)
-let hcons1_constr c =
- let hnames = hcons_names() in
+let hcons1_constr =
+ let hnames = hcons_names () in
let (hc,_,_) = hcons_constr hnames in
- hc c
+ hc
(* Abstract decomposition of constr to deal with generic functions *)
diff --git a/kernel/term.mli b/kernel/term.mli
index d4dbd8ce1..bbd02b6e6 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 68628c63c..670a9f5de 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index d51594822..6e5cdca3e 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/kernel/univ.mli b/kernel/univ.mli
index ba0b6aea1..2460ff15e 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/lib/bij.mli b/lib/bij.mli
index 65bae1eec..7e6d23e82 100644
--- a/lib/bij.mli
+++ b/lib/bij.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Bijections. *)
diff --git a/lib/bstack.mli b/lib/bstack.mli
index d1f9ae387..fc646f1a4 100644
--- a/lib/bstack.mli
+++ b/lib/bstack.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Bounded stacks. If the depth is [None], then there is no depth limit. *)
diff --git a/lib/dyn.mli b/lib/dyn.mli
index 2f2bb7b80..2c0587ee6 100644
--- a/lib/dyn.mli
+++ b/lib/dyn.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Dynamics. Use with extreme care. Not for kids. *)
diff --git a/lib/edit.mli b/lib/edit.mli
index 5926456f0..c86022e44 100644
--- a/lib/edit.mli
+++ b/lib/edit.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* The type of editors.
* An editor is a finite map, ['a -> 'b], which knows how to apply
diff --git a/lib/gmap.mli b/lib/gmap.mli
index 908bad1bc..a73bdba51 100644
--- a/lib/gmap.mli
+++ b/lib/gmap.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Maps using the generic comparison function of ocaml. Same interface as
the module [Map] from the ocaml standard library. *)
diff --git a/lib/gmapl.mli b/lib/gmapl.mli
index c3a55e8c1..23c77851b 100644
--- a/lib/gmapl.mli
+++ b/lib/gmapl.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Maps from ['a] to lists of ['b]. *)
diff --git a/lib/gset.mli b/lib/gset.mli
index 645a29cad..125fbe442 100644
--- a/lib/gset.mli
+++ b/lib/gset.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Sets using the generic comparison function of ocaml. Same interface as
the module [Set] from the ocaml standard library. *)
diff --git a/lib/hashcons.mli b/lib/hashcons.mli
index 9665e1a86..07dd8bc2b 100644
--- a/lib/hashcons.mli
+++ b/lib/hashcons.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Generic hash-consing. *)
diff --git a/lib/options.mli b/lib/options.mli
index 25c194106..d36c6a467 100644
--- a/lib/options.mli
+++ b/lib/options.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Global options of the system. *)
diff --git a/lib/pp.mli b/lib/pp.mli
index 8906616ac..96ef3d3de 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp_control
diff --git a/lib/pp_control.mli b/lib/pp_control.mli
index 6c92849a7..b6d6132e0 100644
--- a/lib/pp_control.mli
+++ b/lib/pp_control.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Parameters of pretty-printing. *)
diff --git a/lib/profile.mli b/lib/profile.mli
index 893bf07b9..6ba6a4489 100644
--- a/lib/profile.mli
+++ b/lib/profile.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Profiling. *)
diff --git a/lib/stamps.mli b/lib/stamps.mli
index 1eb624d57..40a83feb6 100644
--- a/lib/stamps.mli
+++ b/lib/stamps.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Time stamps. *)
diff --git a/lib/system.mli b/lib/system.mli
index 71dff73c3..a91562cea 100644
--- a/lib/system.mli
+++ b/lib/system.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*s Files and load paths. Load path entries remember the original root
given by the user. For efficiency, we keep the full path (field
diff --git a/lib/tlm.mli b/lib/tlm.mli
index 44a2adc8b..f04639750 100644
--- a/lib/tlm.mli
+++ b/lib/tlm.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Tries. This module implements a data structure [('a,'b) t] mapping lists
of values of type ['a] to sets (as lists) of values of type ['b]. *)
diff --git a/lib/util.mli b/lib/util.mli
index 1cb05ad6f..fce150e80 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/library/declare.ml b/library/declare.ml
index 127f60b66..305dd815b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -153,7 +153,16 @@ let (in_constant, out_constant) =
in
declare_object ("CONSTANT", od)
+let hcons_constant_declaration = function
+ | (ConstantEntry ce, stre) ->
+ (ConstantEntry
+ { const_entry_body = hcons1_constr ce.const_entry_body;
+ const_entry_type = option_app hcons1_constr ce.const_entry_type },
+ stre)
+ | cd -> cd
+
let declare_constant id cd =
+ (* let cd = hcons_constant_declaration cd in *)
let sp = add_leaf id CCI (in_constant cd) in
if is_implicit_args() then declare_constant_implicits sp
@@ -228,6 +237,7 @@ let declare_mind mie =
if is_implicit_args() then declare_mib_implicits sp;
sp
+
(*s Test and access functions. *)
let is_constant sp =
diff --git a/library/declare.mli b/library/declare.mli
index 38a14c010..5f9f8ba36 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/global.mli b/library/global.mli
index 05af78a01..0ad3e3713 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/goptions.mli b/library/goptions.mli
index 3cdc122e5..08f5262eb 100644
--- a/library/goptions.mli
+++ b/library/goptions.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* This module manages customization parameters at the vernacular level *)
diff --git a/library/impargs.mli b/library/impargs.mli
index e97a0a41e..bc52caea0 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/indrec.mli b/library/indrec.mli
index 728b3c5dc..8a47c1fae 100644
--- a/library/indrec.mli
+++ b/library/indrec.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/lib.mli b/library/lib.mli
index ed08bcc1d..bc4032a61 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/libobject.mli b/library/libobject.mli
index 17a221a66..7b63af380 100644
--- a/library/libobject.mli
+++ b/library/libobject.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/library.mli b/library/library.mli
index 4d4a2d19b..2f9ee2500 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/library/nametab.mli b/library/nametab.mli
index 7382b447d..13c6b514b 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/library/states.ml b/library/states.ml
index b5c45383d..5a4983a80 100644
--- a/library/states.ml
+++ b/library/states.ml
@@ -12,8 +12,7 @@ let get_state () =
let set_state (fl,fs) =
Lib.unfreeze fl;
- unfreeze_summaries fs;
- Lib.declare_initial_state()
+ unfreeze_summaries fs
let state_magic_number = 19764
diff --git a/library/states.mli b/library/states.mli
index 46cc2f68d..5ff97d103 100644
--- a/library/states.mli
+++ b/library/states.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*s States of the system. In that module, we provide functions to get
and set the state of the whole system. Internally, it is done by
diff --git a/library/summary.mli b/library/summary.mli
index fc639d7f8..feca53fe3 100644
--- a/library/summary.mli
+++ b/library/summary.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/parsing/ast.mli b/parsing/ast.mli
index f40bc78b9..f77ef8123 100755
--- a/parsing/ast.mli
+++ b/parsing/ast.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 6bf724bf8..1541abe64 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/parsing/coqast.mli b/parsing/coqast.mli
index 3a02092cd..38803b5ae 100644
--- a/parsing/coqast.mli
+++ b/parsing/coqast.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Abstract syntax trees. *)
diff --git a/parsing/egrammar.mli b/parsing/egrammar.mli
index c581d9db0..47e477fc5 100644
--- a/parsing/egrammar.mli
+++ b/parsing/egrammar.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Coqast
diff --git a/parsing/esyntax.mli b/parsing/esyntax.mli
index a7da42b9c..fe8542a51 100644
--- a/parsing/esyntax.mli
+++ b/parsing/esyntax.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/parsing/extend.mli b/parsing/extend.mli
index 8fe219d45..086d1b2eb 100644
--- a/parsing/extend.mli
+++ b/parsing/extend.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/parsing/g_minicoq.mli b/parsing/g_minicoq.mli
index db5c0d07f..7ebd65770 100644
--- a/parsing/g_minicoq.mli
+++ b/parsing/g_minicoq.mli
@@ -1,4 +1,6 @@
+(*i $Id$ i*)
+
(*i*)
open Pp
open Names
diff --git a/parsing/g_natsyntax.mli b/parsing/g_natsyntax.mli
index 61f305ad9..f9b7b51d1 100644
--- a/parsing/g_natsyntax.mli
+++ b/parsing/g_natsyntax.mli
@@ -1,4 +1,4 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Nice syntax for naturals. *)
diff --git a/parsing/g_zsyntax.mli b/parsing/g_zsyntax.mli
index 310d09a12..f04d6a151 100644
--- a/parsing/g_zsyntax.mli
+++ b/parsing/g_zsyntax.mli
@@ -1,4 +1,4 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Nice syntax for integers. *)
diff --git a/parsing/lexer.mli b/parsing/lexer.mli
index 2c7351bf1..8ecfbd069 100644
--- a/parsing/lexer.mli
+++ b/parsing/lexer.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
type error =
| Illegal_character
diff --git a/parsing/pattern.mli b/parsing/pattern.mli
index b50f67ed8..5c5c28ba1 100644
--- a/parsing/pattern.mli
+++ b/parsing/pattern.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 7cf26bdd2..26ff04604 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* The lexer and parser of Coq. *)
diff --git a/parsing/pretty.mli b/parsing/pretty.mli
index b8bb0b1a1..0a1ed41f3 100644
--- a/parsing/pretty.mli
+++ b/parsing/pretty.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/parsing/printer.mli b/parsing/printer.mli
index cbc70a2f4..fe456f047 100644
--- a/parsing/printer.mli
+++ b/parsing/printer.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/parsing/search.ml b/parsing/search.ml
index fca710e28..8369ba98c 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -76,7 +76,7 @@ let crible (fn : std_ppcmds -> env -> constr -> unit) ref =
let search_by_head ref =
crible (fun pname ass_name constr ->
let pc = prterm_env ass_name constr in
- mSG[< pname; 'sTR":"; pc; 'fNL >]) ref
+ mSG [< hOV 2 [< pname; 'sTR":"; 'sPC; pc >]; 'fNL >]) ref
(* Fine Search. By Yves Bertot. *)
@@ -96,7 +96,7 @@ let xor a b = (a or b) & (not (a & b))
let plain_display s a c =
let pc = Printer.prterm_env a c in
- mSG [< s; 'sTR":"; pc; 'fNL>]
+ mSG [< hOV 2 [< s; 'sTR":"; 'sPC; pc >]; 'fNL>]
let filter_by_module module_list accept _ _ c =
try
diff --git a/parsing/search.mli b/parsing/search.mli
index 42e277a5d..c0c003ad8 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
open Pp
open Term
diff --git a/parsing/termast.mli b/parsing/termast.mli
index 68ef2f1d0..4b689ead0 100644
--- a/parsing/termast.mli
+++ b/parsing/termast.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index fa9d282ab..b7a04f644 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 342161cb4..19f8a77cd 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
index 038edcb9b..e636f2fbd 100644
--- a/pretyping/coercion.mli
+++ b/pretyping/coercion.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Evd
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 5f3108d48..6d19c624a 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 7d53d3111..f1a247b45 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Term
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index 753bb0fd1..772841e13 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/multcase.mli b/pretyping/multcase.mli
index c0997c044..41cf5561e 100644
--- a/pretyping/multcase.mli
+++ b/pretyping/multcase.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index e91ec8a45..7d93dbb18 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index c7d1665c7..d28732941 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index b0f6615b9..e3233072b 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 8ad0203b3..7d28eeffb 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 4d472c19c..5eee11d19 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/syntax_def.mli b/pretyping/syntax_def.mli
index 7a1116ba0..84ef5e1d9 100644
--- a/pretyping/syntax_def.mli
+++ b/pretyping/syntax_def.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index ede13abea..e17db58c6 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/pretyping/typing.mli b/pretyping/typing.mli
index eaad2791f..8fae1cd41 100644
--- a/pretyping/typing.mli
+++ b/pretyping/typing.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Term
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index aaf9637f8..05baad0ca 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index ac6bc0630..169fde57b 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 1038b5c0d..8591e3367 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 0ea35bea9..8b8e41b34 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index c2b73c85d..043e39170 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 1c1b66077..dbc4ba655 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Environ
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 68767dc8c..f35949580 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Term
diff --git a/proofs/stock.mli b/proofs/stock.mli
index c0cd43c7d..c08a5b480 100644
--- a/proofs/stock.mli
+++ b/proofs/stock.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 800d89051..a23f953e6 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Dyn
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index ee80beba8..a7cf3b6cc 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 26ab1a947..fffe58348 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -1,3 +1,6 @@
+
+(*i $Id$ i*)
+
open Proof_type
open Term
diff --git a/tactics/Inv.v b/tactics/Inv.v
index 1abcdd824..62c77dc8a 100644
--- a/tactics/Inv.v
+++ b/tactics/Inv.v
@@ -68,14 +68,14 @@ Grammar vernac vernac: ast :=
| der_inv_clr_with [ "Derive" "Inversion_clear" identarg($na)
"with" constrarg($com) "." ]
- -> [(MakeInversionLemma $na $com (COMMAND (PROP{Null})))]
+ -> [(MakeInversionLemma $na $com (CONSTR (PROP))) ]
| der_inv_with_srt [ "Derive" "Inversion" identarg($na)
"with" constrarg($com) "Sort" sortarg($s) "." ]
-> [(MakeSemiInversionLemma $na $com $s)]
| der_inv_with [ "Derive" "Inversion" identarg($na) "with" constrarg($com) "." ]
- -> [(MakeSemiInversionLemma $na $com (COMMAND (PROP{Null})))]
+ -> [(MakeSemiInversionLemma $na $com (CONSTR (PROP)))]
| der_inv [ "Derive" "Inversion" identarg($na) identarg($id) "." ]
-> [(MakeSemiInversionLemmaFromHyp 1 $na $id)]
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 14df28f54..24c426d31 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/tactics/autorewrite.mli b/tactics/autorewrite.mli
index bbbc2b047..9215eced3 100644
--- a/tactics/autorewrite.mli
+++ b/tactics/autorewrite.mli
@@ -1,3 +1,6 @@
+
+(*i $Id$ i*)
+
open Tacmach
open Term
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index 237aee4be..ef1aaa50a 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Term
diff --git a/tactics/dhyp.mli b/tactics/dhyp.mli
index de81cce91..2cbf9a827 100644
--- a/tactics/dhyp.mli
+++ b/tactics/dhyp.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 42c6303a0..c39ab011c 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Discrimination nets. *)
diff --git a/tactics/elim.mli b/tactics/elim.mli
index 594dc62ea..af7d17506 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 9e19a0c04..69777da3e 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 183558f60..2c45e831e 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 016134307..16be20610 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Util
diff --git a/tactics/inv.mli b/tactics/inv.mli
index d985bb7aa..39254c763 100644
--- a/tactics/inv.mli
+++ b/tactics/inv.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 238a1a0c5..cec0be893 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -344,9 +344,11 @@ let useInversionLemma =
let gentac =
hide_tactic "UseInversionLemma"
(function
- | [Identifier id;Command com] ->
+ | [Identifier id; Command com] ->
fun gls -> lemInv id (pf_interp_constr gls com) gls
- | l -> anomaly "useInversionLemma" l)
+ | [Identifier id; Constr c] ->
+ fun gls -> lemInv id c gls
+ | _ -> anomaly "useInversionLemma")
in
fun id com -> gentac [Identifier id;Command com]
diff --git a/tactics/nbtermdn.mli b/tactics/nbtermdn.mli
index 038af44d2..7b7da16ef 100644
--- a/tactics/nbtermdn.mli
+++ b/tactics/nbtermdn.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Term
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 50b08265f..86d4e9c34 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
open Term
open Tacmach
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index b364706ca..e12ed0e8c 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Proof_type
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 1f3ede393..256b007fc 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 03ab3a273..335694b7c 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/tactics/termdn.mli b/tactics/termdn.mli
index 8281a3179..044cbf4ff 100644
--- a/tactics/termdn.mli
+++ b/tactics/termdn.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Term
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index b3d372f21..fedea8470 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/toplevel/class.mli b/toplevel/class.mli
index 57d395c20..8c8a64784 100644
--- a/toplevel/class.mli
+++ b/toplevel/class.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/toplevel/command.mli b/toplevel/command.mli
index 8c34a3eb1..ec43a2efb 100644
--- a/toplevel/command.mli
+++ b/toplevel/command.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/toplevel/coqinit.mli b/toplevel/coqinit.mli
index 86b2c9b64..a0b3d5911 100644
--- a/toplevel/coqinit.mli
+++ b/toplevel/coqinit.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Initialization. *)
diff --git a/toplevel/coqtop.mli b/toplevel/coqtop.mli
index 3a97b3b92..53af17474 100644
--- a/toplevel/coqtop.mli
+++ b/toplevel/coqtop.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* The Coq main module. The following function [start] will parse the
command line, print the banner, initialize the load path, load the input
diff --git a/toplevel/discharge.mli b/toplevel/discharge.mli
index 935432f8e..7cd5aab39 100644
--- a/toplevel/discharge.mli
+++ b/toplevel/discharge.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* This module implements the discharge mechanism. It provides a function to
close the last opened section. That function calls [Lib.close_section] and
diff --git a/toplevel/errors.mli b/toplevel/errors.mli
index 4f6a1a074..2fe4e9188 100644
--- a/toplevel/errors.mli
+++ b/toplevel/errors.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/toplevel/fhimsg.mli b/toplevel/fhimsg.mli
index 5680af6f5..7823c7347 100644
--- a/toplevel/fhimsg.mli
+++ b/toplevel/fhimsg.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/toplevel/himsg.mli b/toplevel/himsg.mli
index fabe32634..b67922758 100644
--- a/toplevel/himsg.mli
+++ b/toplevel/himsg.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/toplevel/line_oriented_parser.mli b/toplevel/line_oriented_parser.mli
index 866cfc3df..cfaa1a318 100644
--- a/toplevel/line_oriented_parser.mli
+++ b/toplevel/line_oriented_parser.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
val line_oriented_channel_to_option: string -> in_channel -> int -> char option
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli
index e3d9e593d..fc4ef2968 100644
--- a/toplevel/metasyntax.mli
+++ b/toplevel/metasyntax.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Extend
diff --git a/toplevel/mltop.mli b/toplevel/mltop.mli
index 37a71d212..467395c1e 100644
--- a/toplevel/mltop.mli
+++ b/toplevel/mltop.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* If there is a toplevel under Coq, it is described by the following
record. *)
diff --git a/toplevel/protectedtoplevel.mli b/toplevel/protectedtoplevel.mli
index f618c517f..0046f4a53 100644
--- a/toplevel/protectedtoplevel.mli
+++ b/toplevel/protectedtoplevel.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 842754b9a..c3fbb70f2 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/toplevel/searchisos.mli b/toplevel/searchisos.mli
index 40323c0ec..b6d773cd0 100644
--- a/toplevel/searchisos.mli
+++ b/toplevel/searchisos.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
val search_in_lib : bool ref
val type_search : Term.constr -> unit
diff --git a/toplevel/toplevel.mli b/toplevel/toplevel.mli
index b2509d011..ac807a99a 100644
--- a/toplevel/toplevel.mli
+++ b/toplevel/toplevel.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Pp
diff --git a/toplevel/usage.mli b/toplevel/usage.mli
index 3a4ed2b9b..c89239b6b 100644
--- a/toplevel/usage.mli
+++ b/toplevel/usage.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*s Prints the version number on the standard output and exits (with 0). *)
diff --git a/toplevel/vernac.mli b/toplevel/vernac.mli
index 0c65b8693..5e9c71d19 100644
--- a/toplevel/vernac.mli
+++ b/toplevel/vernac.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Parsing of vernacular. *)
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 47675e0df..fd58ae3ed 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(* Concrete syntax of the mathematical vernacular MV V2.6 *)
@@ -732,7 +732,7 @@ let _ =
fun () ->
begin
start_proof_com (Some s) stre com;
- if (not(is_silent())) then show_open_subgoals()
+ if not (is_silent()) then show_open_subgoals()
end
| _ -> bad_vernac_args "StartProof")
@@ -811,7 +811,7 @@ let _ =
definition_body_red red_option id (local,stre) c typ_opt;
if coe then begin
Class.try_add_new_coercion id stre;
- if (not (is_silent())) then
+ if not (is_silent()) then
message ((string_of_id id) ^ " is now a coercion")
end;
if idcoe then
@@ -1230,7 +1230,7 @@ let _ =
in
fun () ->
Class.try_add_new_class id stre;
- if (not (is_silent())) then
+ if not (is_silent()) then
message ((string_of_id id) ^ " is now a class")
| _ -> bad_vernac_args "CLASS")
@@ -1248,7 +1248,7 @@ let _ =
let isid = identity = "IDENTITY" in
fun () ->
Class.try_add_new_coercion_with_target id stre ids idt isid;
- if (not (is_silent())) then
+ if not (is_silent()) then
message ((string_of_id id) ^ " is now a coercion")
| _ -> bad_vernac_args "COERCION")
diff --git a/toplevel/vernacentries.mli b/toplevel/vernacentries.mli
index 9fbe7574c..68b78ee6a 100644
--- a/toplevel/vernacentries.mli
+++ b/toplevel/vernacentries.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names
diff --git a/toplevel/vernacinterp.mli b/toplevel/vernacinterp.mli
index 4fe1b54c9..0c136820a 100644
--- a/toplevel/vernacinterp.mli
+++ b/toplevel/vernacinterp.mli
@@ -1,5 +1,5 @@
-(* $Id$ *)
+(*i $Id$ i*)
(*i*)
open Names