diff options
| author | filliatr | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr | 2000-12-12 22:07:41 +0000 |
| commit | 8030a420d2cfcf8372d5fe6544efbecde940381b (patch) | |
| tree | 6d4a3c198d4dbecf0cf15f3b53c31447aacfafd7 | |
| parent | faa2647739aa33421328af4ffeaba1bb474e868e (diff) | |
syntaxe AST Inversion + commentaires ocamlweb autour de $
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
133 files changed, 168 insertions, 142 deletions
@@ -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 \ @@ -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 d896d6175e..d4c18da8b9 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 6f1dd08b35..0510d978da 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 84c71f0d7a..827cb34f64 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 b546942e17..c38c6aaa0a 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 3e7d8a9bdc..0cc927c8ca 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 14209cd723..eb6a454806 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 6ab60e2957..2353b6789c 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 00e1084603..71041c279e 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 054a7d3feb..547979fdef 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 9f790e3ca8..a80dcc4359 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 cca174463c..afdcd3a546 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 10b4edc43c..7828ff940e 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 642673a8a3..c0e700a130 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 011d0e414e..7f50c71040 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 38d0580429..5c93bccbf3 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 ff96a8e15b..7a3c7e0533 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 d4dbd8ce17..bbd02b6e60 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 68628c63c2..670a9f5dea 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 d515948222..6e5cdca3e0 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 ba0b6aea19..2460ff15e8 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 65bae1eec2..7e6d23e828 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 d1f9ae387e..fc646f1a4f 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 2f2bb7b802..2c0587ee67 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 5926456f0a..c86022e443 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 908bad1bcf..a73bdba519 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 c3a55e8c1c..23c77851bc 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 645a29cad4..125fbe4422 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 9665e1a86b..07dd8bc2b0 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 25c194106b..d36c6a4678 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 8906616ac4..96ef3d3ded 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 6c92849a78..b6d6132e01 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 893bf07b9e..6ba6a4489b 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 1eb624d57a..40a83feb69 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 71dff73c3b..a91562cea9 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 44a2adc8bf..f046397504 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 1cb05ad6f1..fce150e803 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 127f60b66f..305dd815b8 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 38a14c0107..5f9f8ba36d 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 05af78a01a..0ad3e37136 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 3cdc122e56..08f5262ebf 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 e97a0a41e2..bc52caea05 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 728b3c5dc2..8a47c1faea 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 ed08bcc1d5..bc4032a61d 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 17a221a66a..7b63af380a 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 4d4a2d19b1..2f9ee2500d 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 7382b447da..13c6b514bd 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 b5c45383d9..5a4983a805 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 46cc2f68d1..5ff97d103e 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 fc639d7f83..feca53fe37 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 f40bc78b97..f77ef81239 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 6bf724bf84..1541abe64b 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 3a02092cd4..38803b5ae6 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 c581d9db07..47e477fc5c 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 a7da42b9c1..fe8542a51d 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 8fe219d459..086d1b2ebc 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 db5c0d07f5..7ebd657703 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 61f305ad9c..f9b7b51d1f 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 310d09a12c..f04d6a151d 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 2c7351bf10..8ecfbd0699 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 b50f67ed82..5c5c28ba1b 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 7cf26bdd27..26ff046048 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 b8bb0b1a10..0a1ed41f33 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 cbc70a2f48..fe456f047a 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 fca710e283..8369ba98c2 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 42e277a5d1..c0c003ad8a 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 68ef2f1d0f..4b689ead0b 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 fa9d282ab8..b7a04f6446 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 342161cb44..19f8a77cd6 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 038edcb9bd..e636f2fbd9 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 5f3108d483..6d19c624aa 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 7d53d31118..f1a247b452 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 753bb0fd18..772841e138 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 c0997c044e..41cf5561e7 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 e91ec8a45c..7d93dbb180 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 c7d1665c7a..d28732941d 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 b0f6615b96..e3233072b2 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 8ad0203b35..7d28eeffb7 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 4d472c19c4..5eee11d19c 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 7a1116ba05..84ef5e1d9e 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 ede13abea0..e17db58c63 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 eaad2791f6..8fae1cd416 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 aaf9637f87..05baad0ca1 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 ac6bc06301..169fde57bf 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 1038b5c0d1..8591e33678 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 0ea35bea94..8b8e41b345 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 c2b73c85d4..043e391702 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 1c1b660773..dbc4ba6554 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 68767dc8c1..f359495805 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 c0cd43c7d5..c08a5b4807 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 800d890517..a23f953e6c 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 ee80beba8b..a7cf3b6ccc 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 26ab1a9470..fffe583489 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 1abcdd824f..62c77dc8a0 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 14df28f548..24c426d31b 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 bbbc2b047c..9215eced30 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 237aee4be3..ef1aaa50ae 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 de81cce919..2cbf9a8270 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 42c6303a0c..c39ab011cc 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 594dc62eaf..af7d17506f 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 9e19a0c04d..69777da3e9 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 183558f601..2c45e831e0 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 0161343071..16be20610a 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 d985bb7aaf..39254c7637 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 238a1a0c51..cec0be893f 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 038af44d2d..7b7da16ef2 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 50b08265f4..86d4e9c34f 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 b364706ca1..e12ed0e8ca 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 1f3ede3938..256b007fcc 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 03ab3a2738..335694b7c9 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 8281a31799..044cbf4ff5 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 b3d372f21a..fedea84708 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 57d395c207..8c8a647848 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 8c34a3eb16..ec43a2efb9 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 86b2c9b64e..a0b3d5911b 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 3a97b3b921..53af17474a 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 935432f8eb..7cd5aab39c 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 4f6a1a0743..2fe4e91880 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 5680af6f57..7823c73478 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 fabe326348..b679227581 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 866cfc3df8..cfaa1a3180 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 e3d9e593d7..fc4ef2968a 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 37a71d212c..467395c1ec 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 f618c517f4..0046f4a53b 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 842754b9ad..c3fbb70f23 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 40323c0ec4..b6d773cd02 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 b2509d0119..ac807a99a4 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 3a4ed2b9b4..c89239b6b7 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 0c65b86931..5e9c71d19c 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 47675e0df9..fd58ae3ed5 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 9fbe7574cb..68b78ee6ab 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 4fe1b54c90..0c136820a7 100644 --- a/toplevel/vernacinterp.mli +++ b/toplevel/vernacinterp.mli @@ -1,5 +1,5 @@ -(* $Id$ *) +(*i $Id$ i*) (*i*) open Names |