From 30443ddaba7a0cc996216b3d692b97e0b05907fe Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 11 May 2008 22:04:26 +0000 Subject: - Cleanup parsing of binders, reducing to a single production for all binders. - Change syntax of type class instances to better match the usual syntax of lemmas/definitions with name first, then arguments ":" instance. Update theories/Classes accordingly. - Correct globalization of tactic references when doing Ltac :=/::=, update documentation. - Remove the not so useful "(x &)" and "{{x}}" syntaxes from Program.Utils, and subset_scope as well. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10919 85f007b7-540e-0410-9357-904b9bb8a0f7 --- CHANGES | 1 - contrib/interface/xlate.ml | 4 +- contrib/subtac/g_subtac.ml4 | 9 ++-- doc/refman/RefMan-ltac.tex | 18 ++++--- kernel/names.ml | 1 + kernel/names.mli | 1 + parsing/g_constr.ml4 | 97 ++++++++++++-------------------------- parsing/g_ltac.ml4 | 4 +- parsing/g_vernac.ml4 | 33 +++++++------ parsing/pcoq.ml4 | 2 - parsing/pcoq.mli | 4 +- parsing/ppvernac.ml | 7 +-- tactics/tacinterp.ml | 52 +++++++++++++------- tactics/tacinterp.mli | 2 +- theories/Classes/EquivDec.v | 12 ++--- theories/Classes/Equivalence.v | 14 +++--- theories/Classes/Morphisms.v | 76 ++++++++++++++--------------- theories/Classes/Morphisms_Prop.v | 12 ++--- theories/Classes/RelationClasses.v | 27 +++++------ theories/Classes/SetoidDec.v | 5 +- theories/Classes/SetoidTactics.v | 3 +- theories/Program/Subset.v | 2 +- theories/Program/Syntax.v | 20 ++------ theories/Program/Utils.v | 18 ++----- theories/Program/Wf.v | 14 +++--- toplevel/vernacexpr.ml | 2 +- 26 files changed, 205 insertions(+), 235 deletions(-) diff --git a/CHANGES b/CHANGES index 0fd8c3ac6..a349979fc 100644 --- a/CHANGES +++ b/CHANGES @@ -129,7 +129,6 @@ Tactic Language ltac function into names that do not clash with the lemmas parameter names used in the tactic). - New syntax "Ltac tac ::= ..." to rebind a tactic to a new expression. - (DOC TODO?) - "let rec ... in ... " now supported for expressions without explicit parameters; interpretation is lazy to the contrary of "let ... in ..."; hence, the "rec" keyword can be used to turn the argument of a diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml index 9f7491d5f..9db1c7dc4 100644 --- a/contrib/interface/xlate.ml +++ b/contrib/interface/xlate.ml @@ -1609,8 +1609,8 @@ let rec xlate_vernac = | VernacDeclareTacticDefinition (true, tacs) -> (match List.map (function - ((_, id), _, body) -> - CT_tac_def(CT_ident (string_of_id id), xlate_tactic body)) + (id, _, body) -> + CT_tac_def(reference_to_ct_ID id, xlate_tactic body)) tacs with [] -> assert false | fst::tacs1 -> diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index b7cb7fb23..46bc1a0b8 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -53,7 +53,7 @@ open Constr let sigref = mkRefC (Qualid (dummy_loc, Libnames.qualid_of_string "Coq.Init.Specif.sig")) GEXTEND Gram - GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder_let Constr.binder subtac_nameopt; + GLOBAL: subtac_gallina_loc typeclass_constraint Constr.binder subtac_nameopt; subtac_gallina_loc: [ [ g = Vernac.gallina -> loc, g @@ -66,9 +66,9 @@ GEXTEND Gram ; Constr.binder_let: - [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> + [[ "("; id=Prim.name; ":"; t=Constr.lconstr; "|"; c=Constr.lconstr; ")" -> let typ = mkAppC (sigref, [mkLambdaC ([id], default_binder_kind, t, c)]) in - LocalRawAssum ([id], default_binder_kind, typ) + [LocalRawAssum ([id], default_binder_kind, typ)] ] ]; Constr.binder: @@ -141,7 +141,8 @@ VERNAC COMMAND EXTEND Subtac_Admit_Obligations VERNAC COMMAND EXTEND Subtac_Set_Solver | [ "Obligations" "Tactic" ":=" tactic(t) ] -> [ Coqlib.check_required_library ["Coq";"Program";"Tactics"]; - Tacinterp.add_tacdef false [((dummy_loc, id_of_string "obligations_tactic"), true, t)] ] + Tacinterp.add_tacdef false + [(Qualid (dummy_loc, qualid_of_string "Coq.Program.Tactics.obligations_tactic"), true, t)] ] END VERNAC COMMAND EXTEND Subtac_Show_Obligations diff --git a/doc/refman/RefMan-ltac.tex b/doc/refman/RefMan-ltac.tex index d9a1d4756..fc5f4e4cb 100644 --- a/doc/refman/RefMan-ltac.tex +++ b/doc/refman/RefMan-ltac.tex @@ -187,7 +187,9 @@ is understood as \begin{tabular}{lcl} \nterm{top} & ::= & {\tt Ltac} \nelist{\nterm{ltac\_def}} {\tt with} \\ \\ -\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} {\tacexpr} +\nterm{ltac\_def} & ::= & {\ident} \sequence{\ident}{} {\tt :=} +{\tacexpr}\\ +& $|$ &{\qualid} \sequence{\ident}{} {\tt ::=}{\tacexpr} \end{tabular} \end{centerframe} \caption{Tactic toplevel definitions} @@ -831,11 +833,15 @@ possible with the syntax: {\tacexpr}$_n$ \end{quote} -%This definition bloc is a set of definitions (use of -%the same previous syntactical sugar) and the other scripts are evaluated as -%usual except that the substitutions are lazily carried out (when an identifier -%to be evaluated is the name of a recursive definition). - +It is also possible to \emph{redefine} an existing user-defined tactic +using the syntax: +\begin{quote} +{\tt Ltac} {\qualid} {\ident}$_1$ ... {\ident}$_n$ {\tt ::=} +{\tacexpr} +\end{quote} +A previous definition of \qualid must exist in the environment. +The new definition will always be used instead of the old one and +it goes accross module boundaries. \subsection[Printing {\ltac} tactics]{Printing {\ltac} tactics\comindex{Print Ltac}} diff --git a/kernel/names.ml b/kernel/names.ml index d1c6ee8a4..975390cb9 100644 --- a/kernel/names.ml +++ b/kernel/names.ml @@ -320,6 +320,7 @@ type transparent_state = Idpred.t * Cpred.t let empty_transparent_state = (Idpred.empty, Cpred.empty) let full_transparent_state = (Idpred.full, Cpred.full) let var_full_transparent_state = (Idpred.full, Cpred.empty) +let cst_full_transparent_state = (Idpred.empty, Cpred.full) type 'a tableKey = | ConstKey of constant diff --git a/kernel/names.mli b/kernel/names.mli index 340f6e812..b19f93e2d 100644 --- a/kernel/names.mli +++ b/kernel/names.mli @@ -172,6 +172,7 @@ type transparent_state = Idpred.t * Cpred.t val empty_transparent_state : transparent_state val full_transparent_state : transparent_state val var_full_transparent_state : transparent_state +val cst_full_transparent_state : transparent_state type inv_rel_key = int (* index in the [rel_context] part of environment starting by the end, {\em inverse} diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index ea8d532f9..25a7d0b69 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -23,7 +23,7 @@ open Util let constr_kw = [ "forall"; "fun"; "match"; "fix"; "cofix"; "with"; "in"; "for"; - "end"; "as"; "let"; "dest"; "if"; "then"; "else"; "return"; + "end"; "as"; "let"; "if"; "then"; "else"; "return"; "Prop"; "Set"; "Type"; ".("; "_"; ".." ] let _ = List.iter (fun s -> Lexer.add_token("",s)) constr_kw @@ -129,7 +129,7 @@ let aliasvar = function CPatAlias (_, _, id) -> Some (Name id) | _ -> None GEXTEND Gram GLOBAL: binder_constr lconstr constr operconstr sort global constr_pattern lconstr_pattern Constr.ident - binder binder_let binders_let delimited_binder_let delimited_binders_let + binder binder_let binders_let binders_let_fixannot typeclass_constraint pattern appl_arg; Constr.ident: [ [ id = Prim.ident -> id @@ -210,7 +210,7 @@ GEXTEND Gram mkCProdN loc bl c | "fun"; bl = binder_list; "=>"; c = operconstr LEVEL "200" -> mkCLambdaN loc bl c - | "let"; id=name; bl = LIST0 binder_let; ty = type_cstr; ":="; + | "let"; id=name; bl = binders_let; ty = type_cstr; ":="; c1 = operconstr LEVEL "200"; "in"; c2 = operconstr LEVEL "200" -> let loc1 = loc_of_binder_let bl in CLetIn(loc,id,mkCLambdaN loc1 bl (mk_cast(c1,ty)),c2) @@ -273,13 +273,6 @@ GEXTEND Gram [ [ id=identref; bl=binders_let_fixannot; ty=type_cstr; ":="; c=operconstr LEVEL "200" -> (id,fst bl,snd bl,c,ty) ] ] ; -(* fixannot: *) -(* [ [ "{"; IDENT "struct"; id=name; "}" -> (Some id, CStructRec) *) -(* | "{"; IDENT "wf"; rel=constr; id=OPT name; "}" -> (id, CWfRec rel) *) -(* | "{"; IDENT "measure"; rel=constr; id=OPT name; "}" -> (id, CMeasureRec rel) *) -(* | -> (None, CStructRec) *) -(* ] ] *) -(* ; *) match_constr: [ [ "match"; ci=LIST1 case_item SEP ","; ty=OPT case_type; "with"; br=branches; "end" -> CCases(loc,RegularStyle,ty,ci,br) ] ] @@ -340,24 +333,13 @@ GEXTEND Gram | s = string -> CPatPrim (loc, String s) ] ] ; binder_list: - [ [ idl=LIST1 name; bl=LIST0 binder_let -> - LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl - | idl=LIST1 name; ":"; c=lconstr -> - [LocalRawAssum (idl,Default Explicit,c)] - | cl = binders_let -> cl + [ [ idl=LIST1 name; bl=binders_let -> + LocalRawAssum (idl,Default Explicit,CHole (loc, Some (Evd.BinderType (snd (List.hd idl)))))::bl + | idl=LIST1 name; ":"; c=lconstr -> + [LocalRawAssum (idl,Default Explicit,c)] + | cl = binders_let -> cl ] ] ; - delimited_binders_let: - [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> - ctx @ bl - | b = delimited_binder_let; cl = LIST0 binder_let -> b :: cl - | -> [] ] ] - ; - binders_let: - [ [ "["; ctx = LIST1 typeclass_constraint_binder SEP ","; "]"; bl=binders_let -> - ctx @ bl - | cl = LIST0 binder_let -> cl ] ] - ; binder_assum: [ [ "}" -> fun id -> LocalRawAssum([id], Default Implicit, CHole(loc, None)) | idl=LIST1 name; ":"; c=lconstr; "}" -> @@ -379,51 +361,34 @@ GEXTEND Gram (assum (loc, Name id) :: fst bl), snd bl | f = fixannot -> [], f | b = binder_let; bl = binders_let_fixannot -> - b :: fst bl, snd bl + b @ fst bl, snd bl | -> [], (None, CStructRec) ] ] ; - + binders_let: + [ [ b = binder_let; bl = binders_let -> b @ bl + | -> [] ] ] + ; binder_let: [ [ id=name -> - LocalRawAssum ([id],Default Explicit,CHole (loc, None)) - | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> - LocalRawAssum (id::idl,Default Explicit,c) - | "("; id=name; ":"; c=lconstr; ")" -> - LocalRawAssum ([id],Default Explicit,c) - | "{"; id=name; "}" -> - LocalRawAssum ([id],Default Implicit,CHole (loc, None)) - | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> - LocalRawAssum (id::idl,Default Implicit,c) - | "{"; id=name; ":"; c=lconstr; "}" -> - LocalRawAssum ([id],Default Implicit,c) - | "{"; id=name; idl=LIST1 name; "}" -> - LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)) - | "("; id=name; ":="; c=lconstr; ")" -> - LocalRawDef (id,c) - | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t))) - | "["; tc = typeclass_constraint_binder; "]" -> tc - ] ] - ; - delimited_binder_let: - [ [ "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> - LocalRawAssum (id::idl,Default Explicit,c) - | "("; id=name; ":"; c=lconstr; ")" -> - LocalRawAssum ([id],Default Explicit,c) - | "("; id=name; ":="; c=lconstr; ")" -> - LocalRawDef (id,c) - | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> - LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t))) - | "{"; id=name; "}" -> - LocalRawAssum ([id],Default Implicit,CHole (loc, None)) - | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> - LocalRawAssum (id::idl,Default Implicit,c) - | "{"; id=name; ":"; c=lconstr; "}" -> - LocalRawAssum ([id],Default Implicit,c) - | "{"; id=name; idl=LIST1 name; "}" -> - LocalRawAssum (id::idl,Default Implicit,CHole (loc, None)) - | "["; tc = typeclass_constraint_binder; "]" -> tc + [LocalRawAssum ([id],Default Explicit,CHole (loc, None))] + | "("; id=name; idl=LIST1 name; ":"; c=lconstr; ")" -> + [LocalRawAssum (id::idl,Default Explicit,c)] + | "("; id=name; ":"; c=lconstr; ")" -> + [LocalRawAssum ([id],Default Explicit,c)] + | "("; id=name; ":="; c=lconstr; ")" -> + [LocalRawDef (id,c)] + | "("; id=name; ":"; t=lconstr; ":="; c=lconstr; ")" -> + [LocalRawDef (id,CCast (join_loc (constr_loc t) loc,c, CastConv (DEFAULTcast,t)))] + | "{"; id=name; "}" -> + [LocalRawAssum ([id],Default Implicit,CHole (loc, None))] + | "{"; id=name; idl=LIST1 name; ":"; c=lconstr; "}" -> + [LocalRawAssum (id::idl,Default Implicit,c)] + | "{"; id=name; ":"; c=lconstr; "}" -> + [LocalRawAssum ([id],Default Implicit,c)] + | "{"; id=name; idl=LIST1 name; "}" -> + List.map (fun id -> LocalRawAssum ([id],Default Implicit,CHole (loc, None))) (id::idl) + | "["; tc = LIST1 typeclass_constraint_binder SEP ","; "]" -> tc ] ] ; binder: diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4 index eefbe7da0..cd10e51f1 100644 --- a/parsing/g_ltac.ml4 +++ b/parsing/g_ltac.ml4 @@ -203,9 +203,9 @@ GEXTEND Gram (* Definitions for tactics *) tacdef_body: - [ [ name = identref; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> + [ [ name = Constr.global; it=LIST1 input_fun; redef = ltac_def_kind; body = tactic_expr -> (name, redef, TacFun (it, body)) - | name = identref; redef = ltac_def_kind; body = tactic_expr -> + | name = Constr.global; redef = ltac_def_kind; body = tactic_expr -> (name, redef, body) ] ] ; tactic: diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 3769d7b3e..4eafbd68c 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -157,7 +157,7 @@ GEXTEND Gram ; gallina_ext: [ [ b = record_token; oc = opt_coercion; name = identref; - ps = LIST0 binder_let; + ps = binders_let; s = [ ":"; s = lconstr -> s | -> CSort (loc,Rawterm.RType None) ]; ":="; cstr = OPT identref; "{"; fs = LIST0 record_field SEP ";"; "}" -> @@ -237,7 +237,7 @@ GEXTEND Gram ; (* Inductives and records *) inductive_definition: - [ [ id = identref; indpar = LIST0 binder_let; + [ [ id = identref; indpar = binders_let; c = [ ":"; c = lconstr -> c | -> CSort (loc,Rawterm.RType None) ]; ":="; lc = constructor_list; ntn = decl_notation -> ((id,indpar,c,lc),ntn) ] ] @@ -258,11 +258,11 @@ GEXTEND Gram ; (* (co)-fixpoints *) rec_definition: - [ [ id = ident; b = binder_let; + [ [ id = ident; bl = binders_let_fixannot; ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> - let bl, annot = (b :: fst bl, snd bl) in + let bl, annot = bl in let names = names_of_local_assums bl in let ni = match fst annot with @@ -282,7 +282,7 @@ GEXTEND Gram ((id,(ni,snd annot),bl,ty,def),ntn) ] ] ; corec_definition: - [ [ id = ident; bl = LIST0 binder_let; ty = type_cstr; ":="; + [ [ id = ident; bl = binders_let; ty = type_cstr; ":="; def = lconstr; ntn = decl_notation -> ((id,bl,ty,def),ntn) ] ] ; @@ -337,10 +337,10 @@ GEXTEND Gram (oc,(idl,c)) ] ] ; constructor: - [ [ id = identref; l = LIST0 binder_let; + [ [ id = identref; l = binders_let; coe = of_type_with_opt_coercion; c = lconstr -> (coe,(id,mkCProdN loc l c)) - | id = identref; l = LIST0 binder_let -> + | id = identref; l = binders_let -> (false,(id,mkCProdN loc l (CHole (loc, None)))) ] ] ; of_type_with_opt_coercion: @@ -485,7 +485,7 @@ GEXTEND Gram VernacClass (qid, pars, s, [], props) (* Type classes *) - | IDENT "Class"; sup = OPT [ l = delimited_binders_let; "=>" -> l ]; + | IDENT "Class"; sup = OPT [ l = binders_let; "=>" -> l ]; qid = identref; pars = binders_let; s = [ ":"; c = sort -> Some (loc, c) | -> None ]; props = typeclass_field_types -> @@ -493,15 +493,20 @@ GEXTEND Gram | IDENT "Context"; c = typeclass_context -> VernacContext c - + | global = [ IDENT "Global" -> true | -> false ]; - IDENT "Instance"; sup = OPT [ l = delimited_binders_let ; "=>" -> l ]; - is = typeclass_constraint ; pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs -> + IDENT "Instance"; name = OPT identref; sup = OPT [ l = binders_let -> l ]; +(* name' = OPT [ "=>"; id = identref -> id ]; *) + ":" ; expl = [ "!" -> Rawterm.Implicit | -> Rawterm.Explicit ] ; t = operconstr LEVEL "200"; + pri = OPT [ "|"; i = natural -> i ] ; props = typeclass_field_defs -> let sup = match sup with None -> [] | Some l -> l in let is = (* We reverse the default binding mode on the right *) - let n, bk, t = is in - n, (match bk with Rawterm.Implicit -> Rawterm.Explicit - | Rawterm.Explicit -> Rawterm.Implicit), t + let n = + match name with + | Some (loc, id) -> (loc, Name id) + | None -> (dummy_loc, Anonymous) + in + n, expl, t in VernacInstance (global, sup, is, props, pri) diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 481b73fd0..01b309f3c 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -442,10 +442,8 @@ module Constr = let lconstr_pattern = gec_constr "lconstr_pattern" let binder = Gram.Entry.create "constr:binder" let binder_let = Gram.Entry.create "constr:binder_let" - let delimited_binder_let = Gram.Entry.create "constr:delimited_binder_let" let binders_let = Gram.Entry.create "constr:binders_let" let binders_let_fixannot = Gram.Entry.create "constr:binders_let_fixannot" - let delimited_binders_let = Gram.Entry.create "constr:delimited_binders_let" let typeclass_constraint = Gram.Entry.create "constr:typeclass_constraint" let appl_arg = Gram.Entry.create "constr:appl_arg" end diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 6f6cff275..2525c430a 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -163,11 +163,9 @@ module Constr : val constr_pattern : constr_expr Gram.Entry.e val lconstr_pattern : constr_expr Gram.Entry.e val binder : (name located list * binder_kind * constr_expr) Gram.Entry.e - val binder_let : local_binder Gram.Entry.e - val delimited_binder_let : local_binder Gram.Entry.e + val binder_let : local_binder list Gram.Entry.e val binders_let : local_binder list Gram.Entry.e val binders_let_fixannot : (local_binder list * (identifier located option * recursion_order_expr)) Gram.Entry.e - val delimited_binders_let : local_binder list Gram.Entry.e val typeclass_constraint : (name located * binding_kind * constr_expr) Gram.Entry.e val appl_arg : (constr_expr * explicitation located option) Gram.Entry.e end diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml index 535a4c380..bd87e09c6 100644 --- a/parsing/ppvernac.ml +++ b/parsing/ppvernac.ml @@ -50,7 +50,7 @@ let pr_lname = function (loc,Name id) -> pr_lident (loc,id) | lna -> pr_located pr_name lna -let pr_ltac_id = Nameops.pr_id +let pr_ltac_id = Libnames.pr_reference let pr_module = Libnames.pr_reference @@ -795,13 +795,14 @@ let rec pr_vernac = function match body with | Tacexpr.TacFun (idl,b) -> idl,b | _ -> [], body in - pr_located pr_ltac_id id ++ + pr_ltac_id id ++ prlist (function None -> str " _" | Some id -> spc () ++ pr_id id) idl ++ (if redef then str" ::=" else str" :=") ++ brk(1,1) ++ let idl = List.map Option.get (List.filter (fun x -> not (x=None)) idl)in pr_raw_tactic_env - (idl @ List.map snd (List.map (fun (x, _, _) -> x) l)) + (idl @ List.map coerce_global_to_id + (List.map (fun (x, _, _) -> x) (List.filter (fun (_, redef, _) -> not redef) l))) (Global.env()) body in hov 1 diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index c9dee28d2..58d7e358c 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2655,40 +2655,60 @@ let print_ltac id = errorlabstrm "print_ltac" (pr_qualid id ++ spc() ++ str "is not a user defined tactic") +open Libnames + (* Adds a definition for tactics in the table *) -let make_absolute_name (loc,id) repl = +let make_absolute_name ident repl = + let loc = loc_of_reference ident in try - let kn = if repl then Nametab.locate_tactic (make_short_qualid id) else Lib.make_kn id in + let id, kn = + if repl then None, Nametab.locate_tactic (snd (qualid_of_reference ident)) + else let id = Pcoq.coerce_global_to_id ident in + Some id, Lib.make_kn id + in if Gmap.mem kn !mactab then - if repl then kn + if repl then id, kn else user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is already an Ltac named " ++ pr_id id) + str "There is already an Ltac named " ++ pr_reference ident) else if is_atomic_kn kn then user_err_loc (loc,"Tacinterp.add_tacdef", - str "Reserved Ltac name " ++ pr_id id) - else kn + str "Reserved Ltac name " ++ pr_reference ident) + else id, kn with Not_found -> user_err_loc (loc,"Tacinterp.add_tacdef", - str "There is no Ltac named " ++ pr_id id) + str "There is no Ltac named " ++ pr_reference ident) + +let rec filter_map f l = + let rec aux acc = function + [] -> acc + | hd :: tl -> + match f hd with + Some x -> aux (x :: acc) tl + | None -> aux acc tl + in aux [] l let add_tacdef isrec tacl = -(* let isrec = if !Flags.p1 then isrec else true in*) - let rfun = List.map (fun ((loc,id as locid),b,_) -> (id,make_absolute_name locid b)) tacl in + let rfun = List.map (fun (ident, b, _) -> make_absolute_name ident b) tacl in let ist = - {(make_empty_glob_sign()) with ltacrecvars = if isrec then rfun else []} in + {(make_empty_glob_sign()) with ltacrecvars = + if isrec then filter_map + (function (Some id, qid) -> Some (id, qid) | (None, _) -> None) rfun + else []} in let gtacl = - List.map2 (fun ((_,id),b,def) (_, qid) -> - let k = if b then UpdateTac qid else NewTac id in + List.map2 (fun (_,b,def) (id, qid) -> + let k = if b then UpdateTac qid else NewTac (Option.get id) in let t = Flags.with_option strict_check (intern_tactic ist) def in (k, t)) tacl rfun in let id0 = fst (List.hd rfun) in - let _ = Lib.add_leaf id0 (inMD gtacl) in + let _ = match id0 with Some id0 -> ignore(Lib.add_leaf id0 (inMD gtacl)) + | _ -> Lib.add_anonymous_leaf (inMD gtacl) in List.iter - (fun ((_,id),b,_) -> - if b then Flags.if_verbose msgnl (pr_id id ++ str " is redefined") - else Flags.if_verbose msgnl (pr_id id ++ str " is defined")) + (fun (id,b,_) -> + Flags.if_verbose msgnl (Libnames.pr_reference id ++ + (if b then str " is redefined" + else str " is defined"))) tacl (***************************************************************************) diff --git a/tactics/tacinterp.mli b/tactics/tacinterp.mli index db67d1473..2a490fdac 100644 --- a/tactics/tacinterp.mli +++ b/tactics/tacinterp.mli @@ -63,7 +63,7 @@ val get_debug : unit -> debug_info (* Adds a definition for tactics in the table *) val add_tacdef : - bool -> (identifier Util.located * bool * raw_tactic_expr) list -> unit + bool -> (Libnames.reference * bool * raw_tactic_expr) list -> unit val add_primitive_tactic : string -> glob_tactic_expr -> unit (* Tactic extensions *) diff --git a/theories/Classes/EquivDec.v b/theories/Classes/EquivDec.v index 62744b1d1..d96a532c3 100644 --- a/theories/Classes/EquivDec.v +++ b/theories/Classes/EquivDec.v @@ -94,8 +94,8 @@ Program Instance unit_eqdec : ! EqDec unit eq := reflexivity. Qed. -Program Instance [ EqDec A eq, EqDec B eq ] => - prod_eqdec : ! EqDec (prod A B) eq := +Program Instance prod_eqdec [ EqDec A eq, EqDec B eq ] : + ! EqDec (prod A B) eq := equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in @@ -106,8 +106,8 @@ Program Instance [ EqDec A eq, EqDec B eq ] => Solve Obligations using unfold complement, equiv ; program_simpl. -Program Instance [ EqDec A eq, EqDec B eq ] => - sum_eqdec : ! EqDec (sum A B) eq := +Program Instance sum_eqdec [ EqDec A eq, EqDec B eq ] : + ! EqDec (sum A B) eq := equiv_dec x y := match x, y with | inl a, inl b => if a == b then in_left else in_right @@ -121,7 +121,7 @@ Program Instance [ EqDec A eq, EqDec B eq ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq := +Program Instance bool_function_eqdec [ EqDec A eq ] : ! EqDec (bool -> A) eq := equiv_dec f g := if f true == g true then if f false == g false then in_left @@ -138,7 +138,7 @@ Program Instance [ EqDec A eq ] => bool_function_eqdec : ! EqDec (bool -> A) eq Require Import List. -Program Instance [ eqa : EqDec A eq ] => list_eqdec : ! EqDec (list A) eq := +Program Instance list_eqdec [ eqa : EqDec A eq ] : ! EqDec (list A) eq := equiv_dec := fix aux (x : list A) y { struct x } := match x, y with diff --git a/theories/Classes/Equivalence.v b/theories/Classes/Equivalence.v index 23af8a744..42961baea 100644 --- a/theories/Classes/Equivalence.v +++ b/theories/Classes/Equivalence.v @@ -52,16 +52,16 @@ Infix "=~=" := pequiv (at level 70, no associativity) : equiv_scope. (** Shortcuts to make proof search easier. *) -Program Instance [ sa : Equivalence A ] => equiv_reflexive : Reflexive equiv. +Program Instance equiv_reflexive [ sa : Equivalence A ] : Reflexive equiv. -Program Instance [ sa : Equivalence A ] => equiv_symmetric : Symmetric equiv. +Program Instance equiv_symmetric [ sa : Equivalence A ] : Symmetric equiv. Next Obligation. Proof. symmetry ; auto. Qed. -Program Instance [ sa : Equivalence A ] => equiv_transitive : Transitive equiv. +Program Instance equiv_transitive [ sa : Equivalence A ] : Transitive equiv. Next Obligation. Proof. @@ -116,8 +116,8 @@ Section Respecting. Definition respecting [ Equivalence A (R : relation A), Equivalence B (R' : relation B) ] : Type := { morph : A -> B | respectful R R' morph morph }. - Program Instance [ Equivalence A R, Equivalence B R' ] => - respecting_equiv : Equivalence respecting + Program Instance respecting_equiv [ Equivalence A R, Equivalence B R' ] : + Equivalence respecting (fun (f g : respecting) => forall (x y : A), R x y -> R' (proj1_sig f x) (proj1_sig g y)). Solve Obligations using unfold respecting in * ; simpl_relation ; program_simpl. @@ -134,8 +134,8 @@ End Respecting. (** The default equivalence on function spaces, with higher-priority than [eq]. *) -Program Instance [ Equivalence A eqA ] => - pointwise_equivalence : Equivalence (B -> A) (pointwise_relation eqA) | 9. +Program Instance pointwise_equivalence [ Equivalence A eqA ] : + Equivalence (B -> A) (pointwise_relation eqA) | 9. Next Obligation. Proof. diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v index 5ac6d8ee5..cd38f318c 100644 --- a/theories/Classes/Morphisms.v +++ b/theories/Classes/Morphisms.v @@ -87,12 +87,12 @@ Proof. firstorder. Qed. (** The subrelation property goes through products as usual. *) -Instance [ sub : subrelation A R₁ R₂ ] => - morphisms_subrelation : ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). +Instance morphisms_subrelation [ sub : subrelation A R₁ R₂ ] : + ! subrelation (B -> A) (R ==> R₁) (R ==> R₂). Proof. firstorder. Qed. -Instance [ sub : subrelation A R₂ R₁ ] => - morphisms_subrelation_left : ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. +Instance morphisms_subrelation_left [ sub : subrelation A R₂ R₁ ] : + ! subrelation (A -> B) (R₁ ==> R) (R₂ ==> R) | 3. Proof. firstorder. Qed. (** [Morphism] is itself a covariant morphism for [subrelation]. *) @@ -129,16 +129,15 @@ Proof. firstorder. Qed. Instance iff_inverse_impl_subrelation : subrelation iff (inverse impl). Proof. firstorder. Qed. -Instance [ sub : subrelation A R R' ] => pointwise_subrelation : +Instance pointwise_subrelation [ sub : subrelation A R R' ] : subrelation (pointwise_relation (A:=B) R) (pointwise_relation R') | 4. Proof. reduce. unfold pointwise_relation in *. apply sub. apply H. Qed. (** The complement of a relation conserves its morphisms. *) -Program Instance [ mR : Morphism (A -> A -> Prop) - (RA ==> RA ==> iff) R ] => - complement_morphism : Morphism (RA ==> RA ==> iff) - (complement R). +Program Instance complement_morphism + [ mR : Morphism (A -> A -> Prop) (RA ==> RA ==> iff) R ] : + Morphism (RA ==> RA ==> iff) (complement R). Next Obligation. Proof. @@ -149,8 +148,9 @@ Program Instance [ mR : Morphism (A -> A -> Prop) (** The [inverse] too, actually the [flip] instance is a bit more general. *) -Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => - flip_morphism : Morphism (RB ==> RA ==> RC) (flip f). +Program Instance flip_morphism + [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] : + Morphism (RB ==> RA ==> RC) (flip f). Next Obligation. Proof. @@ -160,8 +160,8 @@ Program Instance [ mor : Morphism (A -> B -> C) (RA ==> RB ==> RC) f ] => (** Every Transitive relation gives rise to a binary morphism on [impl], contravariant in the first argument, covariant in the second. *) -Program Instance [ Transitive A R ] => - trans_contra_co_morphism : Morphism (R --> R ++> impl) R. +Program Instance trans_contra_co_morphism + [ Transitive A R ] : Morphism (R --> R ++> impl) R. Next Obligation. Proof with auto. @@ -181,40 +181,40 @@ Program Instance [ Transitive A R ] => (** Morphism declarations for partial applications. *) -Program Instance [ Transitive A R ] => - trans_contra_inv_impl_morphism : Morphism (R --> inverse impl) (R x). +Program Instance trans_contra_inv_impl_morphism + [ Transitive A R ] : Morphism (R --> inverse impl) (R x). Next Obligation. Proof with auto. transitivity y... Qed. -Program Instance [ Transitive A R ] => - trans_co_impl_morphism : Morphism (R ==> impl) (R x). +Program Instance trans_co_impl_morphism + [ Transitive A R ] : Morphism (R ==> impl) (R x). Next Obligation. Proof with auto. transitivity x0... Qed. -Program Instance [ Transitive A R, Symmetric A R ] => - trans_sym_co_inv_impl_morphism : Morphism (R ==> inverse impl) (R x). +Program Instance trans_sym_co_inv_impl_morphism + [ Transitive A R, Symmetric A R ] : Morphism (R ==> inverse impl) (R x). Next Obligation. Proof with auto. transitivity y... Qed. -Program Instance [ Transitive A R, Symmetric _ R ] => - trans_sym_contra_impl_morphism : Morphism (R --> impl) (R x). +Program Instance trans_sym_contra_impl_morphism + [ Transitive A R, Symmetric _ R ] : Morphism (R --> impl) (R x). Next Obligation. Proof with auto. transitivity x0... Qed. -Program Instance [ Equivalence A R ] => - equivalence_partial_app_morphism : Morphism (R ==> iff) (R x). +Program Instance equivalence_partial_app_morphism + [ Equivalence A R ] : Morphism (R ==> iff) (R x). Next Obligation. Proof with auto. @@ -227,8 +227,8 @@ Program Instance [ Equivalence A R ] => (** Every Transitive relation induces a morphism by "pushing" an [R x y] on the left of an [R x z] proof to get an [R y z] goal. *) -Program Instance [ Transitive A R ] => - trans_co_eq_inv_impl_morphism : Morphism (R ==> (@eq A) ==> inverse impl) R. +Program Instance trans_co_eq_inv_impl_morphism + [ Transitive A R ] : Morphism (R ==> (@eq A) ==> inverse impl) R. Next Obligation. Proof with auto. @@ -245,8 +245,8 @@ Program Instance [ Transitive A R ] => (** Every Symmetric and Transitive relation gives rise to an equivariant morphism. *) -Program Instance [ Transitive A R, Symmetric _ R ] => - trans_sym_morphism : Morphism (R ==> R ==> iff) R. +Program Instance trans_sym_morphism + [ Transitive A R, Symmetric _ R ] : Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -256,8 +256,8 @@ Program Instance [ Transitive A R, Symmetric _ R ] => transitivity y... transitivity y0... Qed. -Program Instance [ Equivalence A R ] => - equiv_morphism : Morphism (R ==> R ==> iff) R. +Program Instance equiv_morphism [ Equivalence A R ] : + Morphism (R ==> R ==> iff) R. Next Obligation. Proof with auto. @@ -288,7 +288,7 @@ Program Instance inverse_iff_impl_id : (* eq_reflexive_morphism : Morphism (@Logic.eq A ==> R) m | 3. *) (* Proof. simpl_relation. Qed. *) -Instance (A : Type) [ Reflexive B R' ] => +Instance reflexive_eq_dom_reflexive (A : Type) [ Reflexive B R' ] : Reflexive (@Logic.eq A ==> R'). Proof. simpl_relation. Qed. @@ -322,12 +322,12 @@ Qed. Class MorphismProxy A (R : relation A) (m : A) : Prop := respect_proxy : R m m. -Instance [ Reflexive A R ] (x : A) => - reflexive_morphism_proxy : MorphismProxy A R x | 1. +Instance reflexive_morphism_proxy + [ Reflexive A R ] (x : A) : MorphismProxy A R x | 1. Proof. firstorder. Qed. -Instance [ Morphism A R x ] => - morphism_morphism_proxy : MorphismProxy A R x | 2. +Instance morphism_morphism_proxy + [ Morphism A R x ] : MorphismProxy A R x | 2. Proof. firstorder. Qed. (* Instance (A : Type) [ Reflexive B R ] => *) @@ -392,8 +392,8 @@ Instance not_inverse_respectful_norm : Normalizes (A -> B) (R ==> inverse R') (inverse (inverse R ==> R')) | 4. Proof. firstorder. Qed. -Instance [ Normalizes B R' (inverse R'') ] => - inverse_respectful_rec_norm : Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')). +Instance inverse_respectful_rec_norm [ Normalizes B R' (inverse R'') ] : + Normalizes (A -> B) (inverse R ==> R') (inverse (R ==> R'')). Proof. red ; intros. pose normalizes as r. setoid_rewrite r. @@ -403,8 +403,8 @@ Qed. (** Once we have normalized, we will apply this instance to simplify the problem. *) -Program Instance [ Morphism A R m ] => - morphism_inverse_morphism : Morphism (inverse R) m | 2. +Program Instance morphism_inverse_morphism + [ Morphism A R m ] : Morphism (inverse R) m | 2. (** Bootstrap !!! *) diff --git a/theories/Classes/Morphisms_Prop.v b/theories/Classes/Morphisms_Prop.v index 301fba534..7dc1f95ef 100644 --- a/theories/Classes/Morphisms_Prop.v +++ b/theories/Classes/Morphisms_Prop.v @@ -73,7 +73,7 @@ Program Instance iff_iff_iff_impl_morphism : Morphism (iff ==> iff ==> iff) impl (** Morphisms for quantifiers *) -Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation iff ==> iff) (@ex A). +Program Instance ex_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@ex A). Next Obligation. Proof. @@ -86,7 +86,7 @@ Program Instance {A : Type} => ex_iff_morphism : Morphism (pointwise_relation if exists x₁. rewrite H. assumption. Qed. -Program Instance {A : Type} => ex_impl_morphism : +Program Instance ex_impl_morphism {A : Type} : Morphism (pointwise_relation impl ==> impl) (@ex A). Next Obligation. @@ -95,7 +95,7 @@ Program Instance {A : Type} => ex_impl_morphism : exists H0. apply H. assumption. Qed. -Program Instance {A : Type} => ex_inverse_impl_morphism : +Program Instance ex_inverse_impl_morphism {A : Type} : Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@ex A). Next Obligation. @@ -104,7 +104,7 @@ Program Instance {A : Type} => ex_inverse_impl_morphism : exists H0. apply H. assumption. Qed. -Program Instance {A : Type} => all_iff_morphism : +Program Instance all_iff_morphism {A : Type} : Morphism (pointwise_relation iff ==> iff) (@all A). Next Obligation. @@ -113,7 +113,7 @@ Program Instance {A : Type} => all_iff_morphism : intuition ; specialize (H x0) ; intuition. Qed. -Program Instance {A : Type} => all_impl_morphism : +Program Instance all_impl_morphism {A : Type} : Morphism (pointwise_relation impl ==> impl) (@all A). Next Obligation. @@ -122,7 +122,7 @@ Program Instance {A : Type} => all_impl_morphism : intuition ; specialize (H x0) ; intuition. Qed. -Program Instance {A : Type} => all_inverse_impl_morphism : +Program Instance all_inverse_impl_morphism {A : Type} : Morphism (pointwise_relation (inverse impl) ==> inverse impl) (@all A). Next Obligation. diff --git a/theories/Classes/RelationClasses.v b/theories/Classes/RelationClasses.v index 015eb7323..25316c278 100644 --- a/theories/Classes/RelationClasses.v +++ b/theories/Classes/RelationClasses.v @@ -65,26 +65,26 @@ Unset Implicit Arguments. (** We can already dualize all these properties. *) -Program Instance [ Reflexive A R ] => flip_Reflexive : Reflexive (flip R) := +Program Instance flip_Reflexive [ Reflexive A R ] : Reflexive (flip R) := reflexivity := reflexivity (R:=R). -Program Instance [ Irreflexive A R ] => flip_Irreflexive : Irreflexive (flip R) := +Program Instance flip_Irreflexive [ Irreflexive A R ] : Irreflexive (flip R) := irreflexivity := irreflexivity (R:=R). -Program Instance [ Symmetric A R ] => flip_Symmetric : Symmetric (flip R). +Program Instance flip_Symmetric [ Symmetric A R ] : Symmetric (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply Symmetric. -Program Instance [ Asymmetric A R ] => flip_Asymmetric : Asymmetric (flip R). +Program Instance flip_Asymmetric [ Asymmetric A R ] : Asymmetric (flip R). Solve Obligations using program_simpl ; unfold flip in * ; intros ; clapply asymmetry. -Program Instance [ Transitive A R ] => flip_Transitive : Transitive (flip R). +Program Instance flip_Transitive [ Transitive A R ] : Transitive (flip R). Solve Obligations using unfold flip ; program_simpl ; clapply transitivity. -Program Instance [ Reflexive A (R : relation A) ] => - Reflexive_complement_Irreflexive : Irreflexive (complement R). +Program Instance Reflexive_complement_Irreflexive [ Reflexive A (R : relation A) ] + : Irreflexive (complement R). Next Obligation. Proof. @@ -95,7 +95,7 @@ Program Instance [ Reflexive A (R : relation A) ] => Qed. -Program Instance [ Symmetric A (R : relation A) ] => complement_Symmetric : Symmetric (complement R). +Program Instance complement_Symmetric [ Symmetric A (R : relation A) ] : Symmetric (complement R). Next Obligation. Proof. @@ -165,8 +165,7 @@ Class PER (carrier : Type) (pequiv : relation carrier) : Prop := (** We can build a PER on the Coq function space if we have PERs on the domain and codomain. *) -Program Instance [ PER A (R : relation A), PER B (R' : relation B) ] => - arrow_per : PER (A -> B) +Program Instance arrow_per [ PER A (R : relation A), PER B (R' : relation B) ] : PER (A -> B) (fun f g => forall (x y : A), R x y -> R' (f x) (g y)). Next Obligation. @@ -188,8 +187,8 @@ Class Equivalence (carrier : Type) (equiv : relation carrier) : Prop := Class [ Equivalence A eqA ] => Antisymmetric (R : relation A) := antisymmetry : forall x y, R x y -> R y x -> eqA x y. -Program Instance [ eq : Equivalence A eqA, ! Antisymmetric eq R ] => - flip_antiSymmetric : Antisymmetric eq (flip R). +Program Instance flip_antiSymmetric [ eq : Equivalence A eqA, ! Antisymmetric eq R ] : + Antisymmetric eq (flip R). (** Leibinz equality [eq] is an equivalence relation. The instance has low priority as it is always applicable @@ -368,7 +367,7 @@ Definition relation_disjunction {A} (R : relation A) (R' : relation A) : relatio (** Relation equivalence is an equivalence, and subrelation defines a partial order. *) -Instance (A : Type) => relation_equivalence_equivalence : +Instance relation_equivalence_equivalence (A : Type) : Equivalence (relation A) relation_equivalence. Proof. intro A. exact (@predicate_equivalence_equivalence (cons A (cons A nil))). Qed. @@ -387,7 +386,7 @@ Class [ equ : Equivalence A eqA, PreOrder A R ] => PartialOrder := for equivalence (see Morphisms). It is also sufficient to show that [R] is antisymmetric w.r.t. [eqA] *) -Instance [ PartialOrder A eqA R ] => partial_order_antisym : ! Antisymmetric A eqA R. +Instance partial_order_antisym [ PartialOrder A eqA R ] : ! Antisymmetric A eqA R. Proof with auto. reduce_goal. pose partial_order_equivalence as poe. do 3 red in poe. apply <- poe. firstorder. diff --git a/theories/Classes/SetoidDec.v b/theories/Classes/SetoidDec.v index 639b15f50..4d6601a6e 100644 --- a/theories/Classes/SetoidDec.v +++ b/theories/Classes/SetoidDec.v @@ -95,8 +95,7 @@ Program Instance unit_eqdec : EqDec (@eq_setoid unit) := reflexivity. Qed. -Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => - prod_eqdec : EqDec (@eq_setoid (prod A B)) := +Program Instance prod_eqdec [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] : EqDec (@eq_setoid (prod A B)) := equiv_dec x y := let '(x1, x2) := x in let '(y1, y2) := y in @@ -111,7 +110,7 @@ Program Instance [ ! EqDec (@eq_setoid A), ! EqDec (@eq_setoid B) ] => Require Import Coq.Program.FunctionalExtensionality. -Program Instance [ ! EqDec (@eq_setoid A) ] => bool_function_eqdec : EqDec (@eq_setoid (bool -> A)) := +Program Instance bool_function_eqdec [ ! EqDec (@eq_setoid A) ] : EqDec (@eq_setoid (bool -> A)) := equiv_dec f g := if f true == g true then if f false == g false then in_left diff --git a/theories/Classes/SetoidTactics.v b/theories/Classes/SetoidTactics.v index 8412cc102..aeaa197e8 100644 --- a/theories/Classes/SetoidTactics.v +++ b/theories/Classes/SetoidTactics.v @@ -38,8 +38,7 @@ Definition default_relation [ DefaultRelation A R ] := R. (** Every [Equivalence] gives a default relation, if no other is given (lowest priority). *) -Instance [ Equivalence A R ] => - equivalence_default : DefaultRelation A R | 4. +Instance equivalence_default [ Equivalence A R ] : DefaultRelation A R | 4. (** The setoid_replace tactics in Ltac, defined in terms of default relations and the setoid_rewrite tactic. *) diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 8ce84c827..c9de1a9e1 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -9,7 +9,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. -Open Local Scope subset_scope. +Open Local Scope program_scope. (** Tactics related to subsets and proof irrelevance. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 6158e88f7..6cd75257b 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,4 +1,4 @@ -(* -*- coq-prog-args: ("-emacs-U" "-nois") -*- *) +(* -*- coq-prog-args: ("-emacs-U") -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) (* y) (at level 100, x,T at level 10, y at next level, no associativity) : program_scope. - (** Notations for the unit type and value. *) Notation " () " := Datatypes.unit : type_scope. @@ -42,11 +38,11 @@ Implicit Arguments cons [[A]]. (** Standard notations for lists. *) -Notation " [] " := nil. -Notation " [ x ] " := (cons x nil). -Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) (at level 1). +Notation " [ ] " := nil : list_scope. +Notation " [ x ] " := (cons x nil) : list_scope. +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. -(** n-ary exists ! *) +(** n-ary exists *) Notation " 'exists' x y , p" := (ex (fun x => (ex (fun y => p)))) (at level 200, x ident, y ident, right associativity) : type_scope. @@ -61,9 +57,3 @@ Tactic Notation "exist" constr(x) := exists x. Tactic Notation "exist" constr(x) constr(y) := exists x ; exists y. Tactic Notation "exist" constr(x) constr(y) constr(z) := exists x ; exists y ; exists z. Tactic Notation "exist" constr(x) constr(y) constr(z) constr(w) := exists x ; exists y ; exists z ; exists w. - -(* Notation " 'Σ' x : T , p" := (sigT (fun x : T => p)) *) -(* (at level 200, x ident, y ident, right associativity) : program_scope. *) - -(* Notation " 'Π' x : T , p " := (forall x : T, p) *) -(* (at level 200, x ident, right associativity) : program_scope. *) \ No newline at end of file diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index 23f0a7d38..c4a20506c 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -12,18 +12,12 @@ Require Export Coq.Program.Tactics. Set Implicit Arguments. -(** Wrap a proposition inside a subset. *) - -Notation " {{ x }} " := (tt : { y : unit | x }). - (** A simpler notation for subsets defined on a cartesian product. *) Notation "{ ( x , y ) : A | P }" := (sig (fun anonymous : A => let (x,y) := anonymous in P)) (x ident, y ident, at level 10) : type_scope. -(** The scope in which programs are typed (not their types). *) - (** Generates an obligation to prove False. *) Notation " ! " := (False_rect _ _) : program_scope. @@ -32,19 +26,12 @@ Delimit Scope program_scope with prg. (** Abbreviation for first projection and hiding of proofs of subset objects. *) -Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : subset_scope. - -Delimit Scope subset_scope with subset. - -(* In [subset_scope] to allow masking by redefinitions for particular types. *) -Notation "( x & ? )" := (@exist _ _ x _) : subset_scope. +Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. (** Coerces objects to their support before comparing them. *) Notation " x '`=' y " := ((x :>) = (y :>)) (at level 70) : program_scope. -(** Quantifying over subsets. *) - Require Import Coq.Bool.Sumbool. (** Construct a dependent disjunction from a boolean. *) @@ -59,10 +46,11 @@ Notation "'in_left'" := (@left _ _ _) : program_scope. Notation "'in_right'" := (@right _ _ _) : program_scope. (** Extraction directives *) - +(* Extraction Inline proj1_sig. Extract Inductive unit => "unit" [ "()" ]. Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) (* Extract Inductive sigT => "prod" [ "" ]. *) +*) \ No newline at end of file diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 20dfe9b01..d24312ff1 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -2,7 +2,7 @@ Require Import Coq.Init.Wf. Require Import Coq.Program.Utils. Require Import ProofIrrelevance. -Open Local Scope subset_scope. +Open Local Scope program_scope. Implicit Arguments Enriching Acc_inv [y]. @@ -91,9 +91,9 @@ Section Well_founded_measure. Variable F_sub : forall x:A, (forall y: { y : A | m y < m x }, P (proj1_sig y)) -> P x. - Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := - F_sub x (fun y: { y : A | m y < m x} => Fix_measure_F_sub (proj1_sig y) - (@Acc_inv _ _ _ r (m (proj1_sig y)) (proj2_sig y))). + Program Fixpoint Fix_measure_F_sub (x : A) (r : Acc lt (m x)) {struct r} : P x := + F_sub x (fun (y : A | m y < m x) => Fix_measure_F_sub y + (@Acc_inv _ _ _ r (m y) (proj2_sig y))). Definition Fix_measure_sub (x : A) := Fix_measure_F_sub x (lt_wf (m x)). @@ -102,7 +102,7 @@ Section Well_founded_measure. Section FixPoint. Variable P : A -> Type. - Variable F_sub : forall x:A, (forall (y : A | m y < m x), P (proj1_sig y)) -> P x. + Program Variable F_sub : forall x:A, (forall (y : A | m y < m x), P y) -> P x. Notation Fix_F := (Fix_measure_F_sub P F_sub) (only parsing). (* alias *) @@ -113,9 +113,9 @@ Section Well_founded_measure. forall (x:A) (f g:forall y : { y : A | m y < m x}, P (`y)), (forall y : { y : A | m y < m x}, f y = g y) -> F_sub x f = F_sub x g. - Lemma Fix_measure_F_eq : + Program Lemma Fix_measure_F_eq : forall (x:A) (r:Acc lt (m x)), - F_sub x (fun (y:{y:A|m y < m x}) => Fix_F (`y) (Acc_inv r (proj2_sig y))) = Fix_F x r. + F_sub x (fun (y:A | m y < m x) => Fix_F y (Acc_inv r (proj2_sig y))) = Fix_F x r. Proof. intros x. set (y := m x). diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml index 22430b7ed..16589805f 100644 --- a/toplevel/vernacexpr.ml +++ b/toplevel/vernacexpr.ml @@ -286,7 +286,7 @@ type vernac_expr = (* Commands *) | VernacDeclareTacticDefinition of - rec_flag * (lident * bool * raw_tactic_expr) list + rec_flag * (reference * bool * raw_tactic_expr) list | VernacHints of locality_flag * lstring list * hints | VernacSyntacticDefinition of identifier * (identifier list * constr_expr) * locality_flag * onlyparsing_flag -- cgit v1.2.3