diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-12 22:07:41 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 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 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 |