diff options
| -rw-r--r-- | API/API.mli | 33 | ||||
| -rw-r--r-- | CHANGES | 4 | ||||
| -rw-r--r-- | interp/dumpglob.ml | 2 | ||||
| -rw-r--r-- | intf/decl_kinds.ml | 3 | ||||
| -rw-r--r-- | intf/vernacexpr.ml | 33 | ||||
| -rw-r--r-- | library/kindops.ml | 48 | ||||
| -rw-r--r-- | library/kindops.mli | 2 | ||||
| -rw-r--r-- | parsing/g_proofs.ml4 | 9 | ||||
| -rw-r--r-- | parsing/g_vernac.ml4 | 90 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 2 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 6 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 64 | ||||
| -rw-r--r-- | stm/vernac_classifier.ml | 21 | ||||
| -rw-r--r-- | vernac/locality.ml | 57 | ||||
| -rw-r--r-- | vernac/locality.mli | 13 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 92 |
16 files changed, 202 insertions, 277 deletions
diff --git a/API/API.mli b/API/API.mli index 1a84600ec..321a0b808 100644 --- a/API/API.mli +++ b/API/API.mli @@ -1302,6 +1302,10 @@ sig | CoFinite | BiFinite + type discharge = + | DoDischarge + | NoDischarge + type locality = | Discharge | Local @@ -1320,6 +1324,7 @@ sig | IdentityCoercion | Instance | Method + | Let type theorem_kind = | Theorem | Lemma @@ -4028,8 +4033,6 @@ sig type verbose_flag = bool - type obsolete_locality = bool - type universe_decl_expr = (lident list, Misctypes.glob_constraint list) gen_universe_decl type ident_decl = lident * universe_decl_expr option @@ -4144,29 +4147,27 @@ sig | VernacRedirect of string * vernac_expr Loc.located | VernacTimeout of int * vernac_expr | VernacFail of vernac_expr - | VernacSyntaxExtension of - bool * obsolete_locality * (lstring * syntax_modifier list) - | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * + | VernacInfix of (lstring * syntax_modifier list) * Constrexpr.constr_expr * scope_name option | VernacNotation of - obsolete_locality * Constrexpr.constr_expr * (lstring * syntax_modifier list) * + Constrexpr.constr_expr * (lstring * syntax_modifier list) * scope_name option | VernacNotationAddFormat of string * string * string - | VernacDefinition of - (Decl_kinds.locality option * Decl_kinds.definition_object_kind) * ident_decl * definition_expr + | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * ident_decl * definition_expr | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of Constrexpr.constr_expr - | VernacAssumption of (Decl_kinds.locality option * Decl_kinds.assumption_object_kind) * + | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) * inline * (ident_decl list * Constrexpr.constr_expr) with_coercion list | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of - Decl_kinds.locality option * (fixpoint_expr * decl_notation list) list + Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list | VernacCoFixpoint of - Decl_kinds.locality option * (cofixpoint_expr * decl_notation list) list + Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -4177,9 +4178,9 @@ sig Libnames.reference option * bool option * Libnames.reference list | VernacImport of bool * Libnames.reference list | VernacCanonical of Libnames.reference Misctypes.or_by_notation - | VernacCoercion of obsolete_locality * Libnames.reference Misctypes.or_by_notation * + | VernacCoercion of Libnames.reference Misctypes.or_by_notation * class_rawexpr * class_rawexpr - | VernacIdentityCoercion of obsolete_locality * lident * + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr | VernacNameSectionHypSet of lident * section_subset_expr | VernacInstance of @@ -4213,9 +4214,9 @@ sig | VernacBackTo of int | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * Libnames.reference list - | VernacHints of obsolete_locality * string list * hints_expr + | VernacHints of string list * hints_expr | VernacSyntacticDefinition of Names.Id.t Loc.located * (Names.Id.t list * Constrexpr.constr_expr) * - obsolete_locality * onlyparsing_flag + onlyparsing_flag | VernacDeclareImplicits of Libnames.reference Misctypes.or_by_notation * (Constrexpr.explicitation * bool * bool) list list | VernacArguments of Libnames.reference Misctypes.or_by_notation * @@ -21,6 +21,10 @@ Tactics - Tactic "decide equality" now able to manage constructors which contain proofs. +Vernacular Commands +- The deprecated Coercion Local, Open Local Scope, Notation Local syntax + was removed. Use Local as a prefix instead. + Changes from 8.7+beta2 to 8.7.0 =============================== diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 13ed65056..0197cf9ae 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -72,7 +72,7 @@ open Decl_kinds let type_of_logical_kind = function | IsDefinition def -> (match def with - | Definition -> "def" + | Definition | Let -> "def" | Coercion -> "coe" | SubClass -> "subclass" | CanonicalStructure -> "canonstruc" diff --git a/intf/decl_kinds.ml b/intf/decl_kinds.ml index a97758833..1dea6d9e9 100644 --- a/intf/decl_kinds.ml +++ b/intf/decl_kinds.ml @@ -8,6 +8,8 @@ (** Informal mathematical status of declarations *) +type discharge = DoDischarge | NoDischarge + type locality = Discharge | Local | Global type binding_kind = Explicit | Implicit @@ -40,6 +42,7 @@ type definition_object_kind = | IdentityCoercion | Instance | Method + | Let type assumption_object_kind = Definitional | Logical | Conjectural diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml index 96bcba5e8..5c9141fd6 100644 --- a/intf/vernacexpr.ml +++ b/intf/vernacexpr.ml @@ -151,10 +151,6 @@ type onlyparsing_flag = Flags.compat_version option If v<>Current, it contains the name of the coq version which this notation is trying to be compatible with *) type locality_flag = bool (* true = Local *) -type obsolete_locality = bool -(* Some grammar entries use obsolete_locality. This bool is to be backward - * compatible. If the grammar is fixed removing deprecated syntax, this - * bool should go away too *) type option_value = Goptions.option_value = | BoolValue of bool @@ -327,31 +323,27 @@ type vernac_expr = | VernacFail of vernac_expr (* Syntax *) - | VernacSyntaxExtension of - bool * obsolete_locality * (lstring * syntax_modifier list) - | VernacOpenCloseScope of obsolete_locality * (bool * scope_name) + | VernacSyntaxExtension of bool * (lstring * syntax_modifier list) + | VernacOpenCloseScope of bool * scope_name | VernacDelimiters of scope_name * string option | VernacBindScope of scope_name * class_rawexpr list - | VernacInfix of obsolete_locality * (lstring * syntax_modifier list) * + | VernacInfix of (lstring * syntax_modifier list) * constr_expr * scope_name option | VernacNotation of - obsolete_locality * constr_expr * (lstring * syntax_modifier list) * + constr_expr * (lstring * syntax_modifier list) * scope_name option | VernacNotationAddFormat of string * string * string (* Gallina *) - | VernacDefinition of - (locality option * definition_object_kind) * ident_decl * definition_expr + | VernacDefinition of (discharge * definition_object_kind) * ident_decl * definition_expr | VernacStartTheoremProof of theorem_kind * proof_expr list | VernacEndProof of proof_end | VernacExactProof of constr_expr - | VernacAssumption of (locality option * assumption_object_kind) * + | VernacAssumption of (discharge * assumption_object_kind) * inline * (ident_decl list * constr_expr) with_coercion list | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list - | VernacFixpoint of - locality option * (fixpoint_expr * decl_notation list) list - | VernacCoFixpoint of - locality option * (cofixpoint_expr * decl_notation list) list + | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list + | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list | VernacScheme of (lident option * scheme) list | VernacCombinedScheme of lident * lident list | VernacUniverse of lident list @@ -364,10 +356,9 @@ type vernac_expr = reference option * export_flag option * reference list | VernacImport of export_flag * reference list | VernacCanonical of reference or_by_notation - | VernacCoercion of obsolete_locality * reference or_by_notation * - class_rawexpr * class_rawexpr - | VernacIdentityCoercion of obsolete_locality * lident * + | VernacCoercion of reference or_by_notation * class_rawexpr * class_rawexpr + | VernacIdentityCoercion of lident * class_rawexpr * class_rawexpr | VernacNameSectionHypSet of lident * section_subset_expr (* Type classes *) @@ -418,9 +409,9 @@ type vernac_expr = (* Commands *) | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * reference list - | VernacHints of obsolete_locality * string list * hints_expr + | VernacHints of string list * hints_expr | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) * - obsolete_locality * onlyparsing_flag + onlyparsing_flag | VernacDeclareImplicits of reference or_by_notation * (explicitation * bool * bool) list list | VernacArguments of reference or_by_notation * diff --git a/library/kindops.ml b/library/kindops.ml index 882f62086..83985ce97 100644 --- a/library/kindops.ml +++ b/library/kindops.ml @@ -23,45 +23,13 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind def = - let (locality, poly, kind) = def in - let error () = CErrors.anomaly (Pp.str "Internal definition kind.") in - match kind with - | Definition -> - begin match locality with - | Discharge -> "Let" - | Local -> "Local Definition" - | Global -> "Definition" - end - | Example -> - begin match locality with - | Discharge -> error () - | Local -> "Local Example" - | Global -> "Example" - end - | Coercion -> - begin match locality with - | Discharge -> error () - | Local -> "Local Coercion" - | Global -> "Coercion" - end - | SubClass -> - begin match locality with - | Discharge -> error () - | Local -> "Local SubClass" - | Global -> "SubClass" - end - | CanonicalStructure -> - begin match locality with - | Discharge -> error () - | Local -> error () - | Global -> "Canonical Structure" - end - | Instance -> - begin match locality with - | Discharge -> error () - | Local -> "Instance" - | Global -> "Global Instance" - end +let string_of_definition_object_kind = function + | Definition -> "Definition" + | Example -> "Example" + | Coercion -> "Coercion" + | SubClass -> "SubClass" + | CanonicalStructure -> "Canonical Structure" + | Instance -> "Instance" + | Let -> "Let" | (StructureComponent|Scheme|CoFixpoint|Fixpoint|IdentityCoercion|Method) -> CErrors.anomaly (Pp.str "Internal definition kind.") diff --git a/library/kindops.mli b/library/kindops.mli index 77979c915..06f873e85 100644 --- a/library/kindops.mli +++ b/library/kindops.mli @@ -12,4 +12,4 @@ open Decl_kinds val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string -val string_of_definition_kind : definition_kind -> string +val string_of_definition_object_kind : definition_object_kind -> string diff --git a/parsing/g_proofs.ml4 b/parsing/g_proofs.ml4 index f10d74677..d88f6fa0d 100644 --- a/parsing/g_proofs.ml4 +++ b/parsing/g_proofs.ml4 @@ -70,19 +70,16 @@ GEXTEND Gram VernacCreateHintDb (id, b) | IDENT "Remove"; IDENT "Hints"; ids = LIST1 global; dbnames = opt_hintbases -> VernacRemoveHints (dbnames, ids) - | IDENT "Hint"; local = obsolete_locality; h = hint; + | IDENT "Hint"; h = hint; dbnames = opt_hintbases -> - VernacHints (local,dbnames, h) + VernacHints (dbnames, h) (* Declare "Resolve" explicitly so as to be able to later extend with "Resolve ->" and "Resolve <-" *) | IDENT "Hint"; IDENT "Resolve"; lc = LIST1 reference_or_constr; info = hint_info; dbnames = opt_hintbases -> - VernacHints (false,dbnames, + VernacHints (dbnames, HintsResolve (List.map (fun x -> (info, true, x)) lc)) ] ]; - obsolete_locality: - [ [ IDENT "Local" -> true | -> false ] ] - ; reference_or_constr: [ [ r = global -> HintsReference r | c = constr -> HintsConstr c ] ] diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 0e585cff7..444f36833 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -149,7 +149,7 @@ GEXTEND Gram | d = def_token; id = ident_decl; b = def_body -> VernacDefinition (d, id, b) | IDENT "Let"; id = identref; b = def_body -> - VernacDefinition ((Some Discharge, Definition), (id, None), b) + VernacDefinition ((DoDischarge, Let), (id, None), b) (* Gallina inductive declarations *) | cum = cumulativity_token; priv = private_token; f = finite_token; indl = LIST1 inductive_definition SEP "with" -> @@ -167,13 +167,13 @@ GEXTEND Gram in VernacInductive (cum, priv,f,indl) | "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (None, recs) + VernacFixpoint (NoDischarge, recs) | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" -> - VernacFixpoint (Some Discharge, recs) + VernacFixpoint (DoDischarge, recs) | "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (None, corecs) + VernacCoFixpoint (NoDischarge, corecs) | IDENT "Let"; "CoFixpoint"; corecs = LIST1 corec_definition SEP "with" -> - VernacCoFixpoint (Some Discharge, corecs) + VernacCoFixpoint (DoDischarge, corecs) | IDENT "Scheme"; l = LIST1 scheme SEP "with" -> VernacScheme l | IDENT "Combined"; IDENT "Scheme"; id = identref; IDENT "from"; l = LIST1 identref SEP "," -> VernacCombinedScheme (id, l) @@ -195,23 +195,23 @@ GEXTEND Gram | IDENT "Property" -> Property ] ] ; def_token: - [ [ "Definition" -> (None, Definition) - | IDENT "Example" -> (None, Example) - | IDENT "SubClass" -> (None, SubClass) ] ] + [ [ "Definition" -> (NoDischarge,Definition) + | IDENT "Example" -> (NoDischarge,Example) + | IDENT "SubClass" -> (NoDischarge,SubClass) ] ] ; assumption_token: - [ [ "Hypothesis" -> (Some Discharge, Logical) - | "Variable" -> (Some Discharge, Definitional) - | "Axiom" -> (None, Logical) - | "Parameter" -> (None, Definitional) - | IDENT "Conjecture" -> (None, Conjectural) ] ] + [ [ "Hypothesis" -> (DoDischarge, Logical) + | "Variable" -> (DoDischarge, Definitional) + | "Axiom" -> (NoDischarge, Logical) + | "Parameter" -> (NoDischarge, Definitional) + | IDENT "Conjecture" -> (NoDischarge, Conjectural) ] ] ; assumptions_token: - [ [ IDENT "Hypotheses" -> ("Hypotheses", (Some Discharge, Logical)) - | IDENT "Variables" -> ("Variables", (Some Discharge, Definitional)) - | IDENT "Axioms" -> ("Axioms", (None, Logical)) - | IDENT "Parameters" -> ("Parameters", (None, Definitional)) - | IDENT "Conjectures" -> ("Conjectures", (None, Conjectural)) ] ] + [ [ IDENT "Hypotheses" -> ("Hypotheses", (DoDischarge, Logical)) + | IDENT "Variables" -> ("Variables", (DoDischarge, Definitional)) + | IDENT "Axioms" -> ("Axioms", (NoDischarge, Logical)) + | IDENT "Parameters" -> ("Parameters", (NoDischarge, Definitional)) + | IDENT "Conjectures" -> ("Conjectures", (NoDischarge, Conjectural)) ] ] ; inline: [ [ IDENT "Inline"; "("; i = INT; ")" -> InlineAt (int_of_string i) @@ -620,34 +620,22 @@ GEXTEND Gram | IDENT "Canonical"; IDENT "Structure"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition - ((Some Global,CanonicalStructure),((Loc.tag s),None),d) + VernacLocal(false, + VernacDefinition ((NoDischarge,CanonicalStructure),((Loc.tag s),None),d)) (* Coercions *) | IDENT "Coercion"; qid = global; d = def_body -> let s = coerce_reference_to_id qid in - VernacDefinition ((None,Coercion),((Loc.tag s),None),d) - | IDENT "Coercion"; IDENT "Local"; qid = global; d = def_body -> - let s = coerce_reference_to_id qid in - VernacDefinition ((Some Decl_kinds.Local,Coercion),((Loc.tag s),None),d) - | IDENT "Identity"; IDENT "Coercion"; IDENT "Local"; f = identref; - ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (true, f, s, t) + VernacDefinition ((NoDischarge,Coercion),((Loc.tag s),None),d) | IDENT "Identity"; IDENT "Coercion"; f = identref; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacIdentityCoercion (false, f, s, t) - | IDENT "Coercion"; IDENT "Local"; qid = global; ":"; - s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (true, AN qid, s, t) - | IDENT "Coercion"; IDENT "Local"; ntn = by_notation; ":"; - s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (true, ByNotation ntn, s, t) + VernacIdentityCoercion (f, s, t) | IDENT "Coercion"; qid = global; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (false, AN qid, s, t) + VernacCoercion (AN qid, s, t) | IDENT "Coercion"; ntn = by_notation; ":"; s = class_rawexpr; ">->"; t = class_rawexpr -> - VernacCoercion (false, ByNotation ntn, s, t) + VernacCoercion (ByNotation ntn, s, t) | IDENT "Context"; c = binders -> VernacContext c @@ -1106,11 +1094,11 @@ GEXTEND Gram GLOBAL: syntax; syntax: - [ [ IDENT "Open"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (local,(true,sc)) + [ [ IDENT "Open"; IDENT "Scope"; sc = IDENT -> + VernacOpenCloseScope (true,sc) - | IDENT "Close"; local = obsolete_locality; IDENT "Scope"; sc = IDENT -> - VernacOpenCloseScope (local,(false,sc)) + | IDENT "Close"; IDENT "Scope"; sc = IDENT -> + VernacOpenCloseScope (false,sc) | IDENT "Delimit"; IDENT "Scope"; sc = IDENT; "with"; key = IDENT -> VernacDelimiters (sc, Some key) @@ -1120,32 +1108,31 @@ GEXTEND Gram | IDENT "Bind"; IDENT "Scope"; sc = IDENT; "with"; refl = LIST1 class_rawexpr -> VernacBindScope (sc,refl) - | IDENT "Infix"; local = obsolete_locality; - op = ne_lstring; ":="; p = constr; + | IDENT "Infix"; op = ne_lstring; ":="; p = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacInfix (local,(op,modl),p,sc) - | IDENT "Notation"; local = obsolete_locality; id = identref; + VernacInfix ((op,modl),p,sc) + | IDENT "Notation"; id = identref; idl = LIST0 ident; ":="; c = constr; b = only_parsing -> VernacSyntacticDefinition - (id,(idl,c),local,b) - | IDENT "Notation"; local = obsolete_locality; s = lstring; ":="; + (id,(idl,c),b) + | IDENT "Notation"; s = lstring; ":="; c = constr; modl = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ]; sc = OPT [ ":"; sc = IDENT -> sc ] -> - VernacNotation (local,c,(s,modl),sc) + VernacNotation (c,(s,modl),sc) | IDENT "Format"; IDENT "Notation"; n = STRING; s = STRING; fmt = STRING -> VernacNotationAddFormat (n,s,fmt) | IDENT "Reserved"; IDENT "Infix"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] -> let (loc,s) = s in - VernacSyntaxExtension (true, false,((loc,"x '"^s^"' y"),l)) + VernacSyntaxExtension (true,((loc,"x '"^s^"' y"),l)) - | IDENT "Reserved"; IDENT "Notation"; local = obsolete_locality; + | IDENT "Reserved"; IDENT "Notation"; s = ne_lstring; l = [ "("; l = LIST1 syntax_modifier SEP ","; ")" -> l | -> [] ] - -> VernacSyntaxExtension (false, local,(s,l)) + -> VernacSyntaxExtension (false, (s,l)) (* "Print" "Grammar" should be here but is in "command" entry in order to factorize with other "Print"-based vernac entries *) @@ -1158,9 +1145,6 @@ GEXTEND Gram Some (parse_compat_version s) | -> None ] ] ; - obsolete_locality: - [ [ IDENT "Local" -> true | -> false ] ] - ; level: [ [ IDENT "level"; n = natural -> NumLevel n | IDENT "next"; IDENT "level" -> NextLevel ] ] diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 829556a71..87609296b 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -154,7 +154,7 @@ VERNAC COMMAND EXTEND Function | _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in match Vernac_classifier.classify_vernac - (Vernacexpr.VernacFixpoint(None, List.map snd recsl)) + (Vernacexpr.VernacFixpoint(Decl_kinds.NoDischarge, List.map snd recsl)) with | Vernacexpr.VtSideff ids, _ when hard -> Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater) diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 7385ed84c..3efb7b914 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -551,9 +551,9 @@ GEXTEND Gram | IDENT "Canonical"; qid = Constr.global; d = G_vernac.def_body -> let s = coerce_reference_to_id qid in - Vernacexpr.VernacDefinition - ((Some Decl_kinds.Global,Decl_kinds.CanonicalStructure), - ((Loc.tag s),None),(d )) + Vernacexpr.VernacLocal(false,Vernacexpr.VernacDefinition + ((Decl_kinds.NoDischarge,Decl_kinds.CanonicalStructure), + ((Loc.tag s),None),(d ))) ]]; END diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 1a74538aa..46ef2ac03 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -324,23 +324,18 @@ open Decl_kinds | SortClass -> keyword "Sortclass" | RefClass qid -> pr_smart_global qid - let pr_assumption_token many (l,a) = - let l = match l with Some x -> x | None -> Decl_kinds.Global in - match l, a with - | (Discharge,Logical) -> - keyword (if many then "Hypotheses" else "Hypothesis") - | (Discharge,Definitional) -> - keyword (if many then "Variables" else "Variable") - | (Global,Logical) -> + let pr_assumption_token many discharge kind = + match discharge, kind with + | (NoDischarge,Logical) -> keyword (if many then "Axioms" else "Axiom") - | (Global,Definitional) -> + | (NoDischarge,Definitional) -> keyword (if many then "Parameters" else "Parameter") - | (Local, Logical) -> - keyword (if many then "Local Axioms" else "Local Axiom") - | (Local,Definitional) -> - keyword (if many then "Local Parameters" else "Local Parameter") - | (Global,Conjectural) -> str"Conjecture" - | ((Discharge | Local),Conjectural) -> + | (NoDischarge,Conjectural) -> str"Conjecture" + | (DoDischarge,Logical) -> + keyword (if many then "Hypotheses" else "Hypothesis") + | (DoDischarge,Definitional) -> + keyword (if many then "Variables" else "Variable") + | (DoDischarge,Conjectural) -> anomaly (Pp.str "Don't know how to beautify a local conjecture.") let pr_params pr_c (xl,(c,t)) = @@ -631,7 +626,7 @@ open Decl_kinds return (keyword "Fail" ++ spc() ++ pr_vernac_body v) (* Syntax *) - | VernacOpenCloseScope (_,(opening,sc)) -> + | VernacOpenCloseScope (opening,sc) -> return ( keyword (if opening then "Open " else "Close ") ++ keyword "Scope" ++ spc() ++ str sc @@ -660,7 +655,7 @@ open Decl_kinds ++ spc() ++ pr_smart_global q ++ spc() ++ str"[" ++ prlist_with_sep sep pr_opt_scope scl ++ str"]" ) - | VernacInfix (_,((_,s),mv),q,sn) -> (* A Verifier *) + | VernacInfix (((_,s),mv),q,sn) -> (* A Verifier *) return ( hov 0 (hov 0 (keyword "Infix " ++ qs s ++ str " :=" ++ pr_constrarg q) ++ @@ -669,7 +664,7 @@ open Decl_kinds | None -> mt() | Some sc -> spc() ++ str":" ++ spc() ++ str sc)) ) - | VernacNotation (_,c,((_,s),l),opt) -> + | VernacNotation (c,((_,s),l),opt) -> return ( hov 2 (keyword "Notation" ++ spc() ++ qs s ++ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++ @@ -677,7 +672,7 @@ open Decl_kinds | None -> mt() | Some sc -> str" :" ++ spc() ++ str sc)) ) - | VernacSyntaxExtension (_, _,(s,l)) -> + | VernacSyntaxExtension (_, (s, l)) -> return ( keyword "Reserved Notation" ++ spc() ++ pr_located qs s ++ pr_syntax_modifiers l @@ -688,10 +683,9 @@ open Decl_kinds ) (* Gallina *) - | VernacDefinition (d,id,b) -> (* A verifier... *) - let pr_def_token (l,dk) = - let l = match l with Some x -> x | None -> Decl_kinds.Global in - keyword (Kindops.string_of_definition_kind (l,false,dk)) + | VernacDefinition ((discharge,kind),id,b) -> (* A verifier... *) + let pr_def_token dk = + keyword (Kindops.string_of_definition_object_kind dk) in let pr_reduce = function | None -> mt() @@ -712,7 +706,7 @@ open Decl_kinds let (binds,typ,c) = pr_def_body b in return ( hov 2 ( - pr_def_token d ++ spc() + pr_def_token kind ++ spc() ++ pr_ident_decl id ++ binds ++ typ ++ (match c with | None -> mt() @@ -737,13 +731,13 @@ open Decl_kinds ) | VernacExactProof c -> return (hov 2 (keyword "Proof" ++ pr_lconstrarg c)) - | VernacAssumption (stre,t,l) -> + | VernacAssumption ((discharge,kind),t,l) -> let n = List.length (List.flatten (List.map fst (List.map snd l))) in let pr_params (c, (xl, t)) = hov 2 (prlist_with_sep sep pr_ident_decl xl ++ spc() ++ (if c then str":>" else str":" ++ spc() ++ pr_lconstr_expr t)) in let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in - return (hov 2 (pr_assumption_token (n > 1) stre ++ + return (hov 2 (pr_assumption_token (n > 1) discharge kind ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = @@ -793,9 +787,8 @@ open Decl_kinds | VernacFixpoint (local, recs) -> let local = match local with - | Some Discharge -> "Let " - | Some Local -> "Local " - | None | Some Global -> "" + | DoDischarge -> "Let " + | NoDischarge -> "" in return ( hov 0 (str local ++ keyword "Fixpoint" ++ spc () ++ @@ -805,9 +798,8 @@ open Decl_kinds | VernacCoFixpoint (local, corecs) -> let local = match local with - | Some Discharge -> keyword "Let" ++ spc () - | Some Local -> keyword "Local" ++ spc () - | None | Some Global -> str "" + | DoDischarge -> keyword "Let" ++ spc () + | NoDischarge -> str "" in let pr_onecorec ((iddecl,bl,c,def),ntn) = pr_ident_decl iddecl ++ spc() ++ pr_binders bl ++ spc() ++ str":" ++ @@ -868,14 +860,14 @@ open Decl_kinds return ( keyword "Canonical Structure" ++ spc() ++ pr_smart_global q ) - | VernacCoercion (_,id,c1,c2) -> + | VernacCoercion (id,c1,c2) -> return ( hov 1 ( keyword "Coercion" ++ spc() ++ pr_smart_global id ++ spc() ++ str":" ++ spc() ++ pr_class_rawexpr c1 ++ spc() ++ str">->" ++ spc() ++ pr_class_rawexpr c2) ) - | VernacIdentityCoercion (_,id,c1,c2) -> + | VernacIdentityCoercion (id,c1,c2) -> return ( hov 1 ( keyword "Identity Coercion" ++ spc() ++ pr_lident id ++ @@ -999,9 +991,9 @@ open Decl_kinds prlist_with_sep spc (fun r -> pr_id (coerce_reference_to_id r)) ids ++ pr_opt_hintbases dbnames) ) - | VernacHints (_, dbnames,h) -> + | VernacHints (dbnames,h) -> return (pr_hints dbnames h pr_constr pr_constr_pattern_expr) - | VernacSyntacticDefinition (id,(ids,c),_,compat) -> + | VernacSyntacticDefinition (id,(ids,c),compat) -> return ( hov 2 (keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++ diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml index 3aa2cd707..1ca572a36 100644 --- a/stm/vernac_classifier.ml +++ b/stm/vernac_classifier.ml @@ -103,8 +103,7 @@ let rec classify_vernac e = | VernacUnsetOption (["Default";"Proof";"Using"]) | VernacSetOption (["Default";"Proof";"Using"],_) -> VtSideff [], VtNow (* StartProof *) - | VernacDefinition ( - (Some Decl_kinds.Discharge,Decl_kinds.Definition),((_,i),_),ProveBody _) -> + | VernacDefinition ((Decl_kinds.DoDischarge,_),((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),Doesn'tGuaranteeOpacity,[i]), VtLater | VernacDefinition (_,((_,i),_),ProveBody _) -> VtStartProof(default_proof_mode (),GuaranteesOpacity,[i]), VtLater @@ -113,19 +112,29 @@ let rec classify_vernac e = CList.map_filter (function (Some ((_,i),pl), _) -> Some i | _ -> None) l in VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater | VernacGoal _ -> VtStartProof (default_proof_mode (),GuaranteesOpacity,[]), VtLater - | VernacFixpoint (_,l) -> + | VernacFixpoint (discharge,l) -> + let guarantee = + match discharge with + | Decl_kinds.NoDischarge -> GuaranteesOpacity + | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + in let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater - | VernacCoFixpoint (_,l) -> + | VernacCoFixpoint (discharge,l) -> + let guarantee = + match discharge with + | Decl_kinds.NoDischarge -> GuaranteesOpacity + | Decl_kinds.DoDischarge -> Doesn'tGuaranteeOpacity + in let ids, open_proof = List.fold_left (fun (l,b) ((((_,id),_),_,_,p),_) -> id::l, b || p = None) ([],false) l in if open_proof - then VtStartProof (default_proof_mode (),GuaranteesOpacity,ids), VtLater + then VtStartProof (default_proof_mode (),guarantee,ids), VtLater else VtSideff ids, VtLater (* Sideff: apply to all open branches. usually run on master only *) | VernacAssumption (_,_,l) -> diff --git a/vernac/locality.ml b/vernac/locality.ml index 681b1ab20..87b411625 100644 --- a/vernac/locality.ml +++ b/vernac/locality.ml @@ -6,36 +6,14 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) +open Decl_kinds + (** * Managing locality *) let local_of_bool = function - | true -> Decl_kinds.Local - | false -> Decl_kinds.Global - -(** Extracting the locality flag *) - -(* Commands which supported an inlined Local flag *) - -let warn_deprecated_local_syntax = - CWarnings.create ~name:"deprecated-local-syntax" ~category:"deprecated" - (fun () -> - Pp.strbrk "Deprecated syntax: use \"Local\" as a prefix.") - -let enforce_locality_full locality_flag local = - let local = - match locality_flag with - | Some false when local -> - CErrors.user_err Pp.(str "Cannot be simultaneously Local and Global.") - | Some true when local -> - CErrors.user_err Pp.(str "Use only prefix \"Local\".") - | None -> - if local then begin - warn_deprecated_local_syntax (); - Some true - end else - None - | Some b -> Some b in - local + | true -> Local + | false -> Global + (** Positioning locality for commands supporting discharging and export outside of modules *) @@ -48,15 +26,16 @@ let make_non_locality = function Some false -> false | _ -> true let make_locality = function Some true -> true | _ -> false -let enforce_locality locality_flag local = - make_locality (enforce_locality_full locality_flag local) +let enforce_locality_exp locality_flag discharge = + match locality_flag, discharge with + | Some b, NoDischarge -> local_of_bool b + | None, NoDischarge -> Global + | None, DoDischarge -> Discharge + | Some true, DoDischarge -> CErrors.user_err Pp.(str "Local not allowed in this case") + | Some false, DoDischarge -> CErrors.user_err Pp.(str "Global not allowed in this case") -let enforce_locality_exp locality_flag local = - match locality_flag, local with - | None, Some local -> local - | Some b, None -> local_of_bool b - | None, None -> Decl_kinds.Global - | Some _, Some _ -> CErrors.user_err Pp.(str "Local non allowed in this case") +let enforce_locality locality_flag = + make_locality locality_flag (* For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; @@ -65,8 +44,8 @@ let enforce_locality_exp locality_flag local = let make_section_locality = function Some b -> b | None -> Lib.sections_are_opened () -let enforce_section_locality locality_flag local = - make_section_locality (enforce_locality_full locality_flag local) +let enforce_section_locality locality_flag = + make_section_locality locality_flag (** Positioning locality for commands supporting export but not discharge *) @@ -83,5 +62,5 @@ let make_module_locality = function | Some true -> true | None -> false -let enforce_module_locality locality_flag local = - make_module_locality (enforce_locality_full locality_flag local) +let enforce_module_locality locality_flag = + make_module_locality locality_flag diff --git a/vernac/locality.mli b/vernac/locality.mli index bef66d8bc..922538b23 100644 --- a/vernac/locality.mli +++ b/vernac/locality.mli @@ -8,10 +8,6 @@ (** * Managing locality *) -(** Commands which supported an inlined Local flag *) - -val enforce_locality_full : bool option -> bool -> bool option - (** * Positioning locality for commands supporting discharging and export outside of modules *) @@ -22,16 +18,15 @@ val enforce_locality_full : bool option -> bool -> bool option val make_locality : bool option -> bool val make_non_locality : bool option -> bool -val enforce_locality : bool option -> bool -> bool -val enforce_locality_exp : - bool option -> Decl_kinds.locality option -> Decl_kinds.locality +val enforce_locality_exp : bool option -> Decl_kinds.discharge -> Decl_kinds.locality +val enforce_locality : bool option -> bool (** For commands whose default is to not discharge but to export: Global in sections forces discharge, Global not in section is the default; Local in sections is the default, Local not in section forces non-export *) val make_section_locality : bool option -> bool -val enforce_section_locality : bool option -> bool -> bool +val enforce_section_locality : bool option -> bool (** * Positioning locality for commands supporting export but not discharge *) @@ -40,4 +35,4 @@ val enforce_section_locality : bool option -> bool -> bool Local in sections is the default, Local not in section forces non-export *) val make_module_locality : bool option -> bool -val enforce_module_locality : bool option -> bool -> bool +val enforce_module_locality : bool option -> bool diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 7f3410bc1..1d9cb65f1 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -409,8 +409,8 @@ let dump_global r = (**********) (* Syntax *) -let vernac_syntax_extension atts local infix l = - let local = enforce_module_locality atts.locality local in +let vernac_syntax_extension atts infix l = + let local = enforce_module_locality atts.locality in if infix then Metasyntax.check_infix_modifiers (snd l); Metasyntax.add_syntax_extension local l @@ -421,20 +421,20 @@ let vernac_delimiters sc = function let vernac_bind_scope sc cll = Metasyntax.add_class_scope sc (List.map scope_class_of_qualid cll) -let vernac_open_close_scope ~atts local (b,s) = - let local = enforce_section_locality atts.locality local in +let vernac_open_close_scope ~atts (b,s) = + let local = enforce_section_locality atts.locality in Notation.open_close_scope (local,b,s) let vernac_arguments_scope ~atts r scl = let local = make_section_locality atts.locality in Notation.declare_arguments_scope local (smart_global r) scl -let vernac_infix ~atts local = - let local = enforce_module_locality atts.locality local in +let vernac_infix ~atts = + let local = enforce_module_locality atts.locality in Metasyntax.add_infix local (Global.env()) -let vernac_notation ~atts local = - let local = enforce_module_locality atts.locality local in +let vernac_notation ~atts = + let local = enforce_module_locality atts.locality in Metasyntax.add_notation local (Global.env()) (***********) @@ -472,16 +472,16 @@ let vernac_definition_hook p = function | SubClass -> Class.add_subclass_hook p | _ -> no_hook -let vernac_definition ~atts (local,k) ((loc,id as lid),pl) def = - let local = enforce_locality_exp atts.locality local in - let hook = vernac_definition_hook atts.polymorphic k in +let vernac_definition ~atts discharge kind ((loc,id as lid),pl) def = + let local = enforce_locality_exp atts.locality discharge in + let hook = vernac_definition_hook atts.polymorphic kind in let () = match local with | Discharge -> Dumpglob.dump_definition lid true "var" | Local | Global -> Dumpglob.dump_definition lid false "def" in (match def with | ProveBody (bl,t) -> (* local binders, typ *) - start_proof_and_print (local, atts.polymorphic, DefinitionBody k) + start_proof_and_print (local, atts.polymorphic, DefinitionBody kind) [Some (lid,pl), (bl,t)] hook | DefineBody (bl,red_option,c,typ_opt) -> let red_option = match red_option with @@ -489,10 +489,10 @@ let vernac_definition ~atts (local,k) ((loc,id as lid),pl) def = | Some r -> let sigma, env = Pfedit.get_current_context () in Some (snd (Hook.get f_interp_redexp env sigma r)) in - do_definition id (local, atts.polymorphic,k) pl bl red_option c typ_opt hook) + do_definition id (local, atts.polymorphic, kind) pl bl red_option c typ_opt hook) let vernac_start_proof ~atts kind l = - let local = enforce_locality_exp atts.locality None in + let local = enforce_locality_exp atts.locality NoDischarge in if Dumpglob.dump () then List.iter (fun (id, _) -> match id with @@ -511,8 +511,8 @@ let vernac_exact_proof c = save_proof (Vernacexpr.(Proved(Opaque,None))); if not status then Feedback.feedback Feedback.AddedAxiom -let vernac_assumption ~atts (local, kind) l nl = - let local = enforce_locality_exp atts.locality local in +let vernac_assumption ~atts discharge kind l nl = + let local = enforce_locality_exp atts.locality discharge in let global = local == Global in let kind = local, atts.polymorphic, kind in List.iter (fun (is_coe,(idl,c)) -> @@ -594,14 +594,14 @@ let vernac_inductive ~atts cum lo finite indl = let indl = List.map unpack indl in do_mutual_inductive indl is_cumulative atts.polymorphic lo finite -let vernac_fixpoint ~atts local l = - let local = enforce_locality_exp atts.locality local in +let vernac_fixpoint ~atts discharge l = + let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_fixpoint local atts.polymorphic l -let vernac_cofixpoint ~atts local l = - let local = enforce_locality_exp atts.locality local in +let vernac_cofixpoint ~atts discharge l = + let local = enforce_locality_exp atts.locality discharge in if Dumpglob.dump () then List.iter (fun (((lid,_), _, _, _), _) -> Dumpglob.dump_definition lid false "def") l; do_cofixpoint local atts.polymorphic l @@ -812,16 +812,16 @@ let vernac_require from import qidl = let vernac_canonical r = Recordops.declare_canonical_structure (smart_global r) -let vernac_coercion ~atts local ref qids qidt = - let local = enforce_locality atts.locality local in +let vernac_coercion ~atts ref qids qidt = + let local = enforce_locality atts.locality in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in let ref' = smart_global ref in Class.try_add_new_coercion_with_target ref' ~local atts.polymorphic ~source ~target; Flags.if_verbose Feedback.msg_info (pr_global ref' ++ str " is now a coercion") -let vernac_identity_coercion ~atts local id qids qidt = - let local = enforce_locality atts.locality local in +let vernac_identity_coercion ~atts id qids qidt = + let local = enforce_locality atts.locality in let target = cl_of_qualid qidt in let source = cl_of_qualid qids in Class.try_add_new_identity_coercion id ~local atts.polymorphic ~source ~target @@ -947,13 +947,13 @@ let vernac_remove_hints ~atts dbs ids = let local = make_module_locality atts.locality in Hints.remove_hints local dbs (List.map Smartlocate.global_with_alias ids) -let vernac_hints ~atts local lb h = - let local = enforce_module_locality atts.locality local in +let vernac_hints ~atts lb h = + let local = enforce_module_locality atts.locality in Hints.add_hints local lb (Hints.interp_hints atts.polymorphic h) -let vernac_syntactic_definition ~atts lid x local y = +let vernac_syntactic_definition ~atts lid x y = Dumpglob.dump_definition lid false "syndef"; - let local = enforce_module_locality atts.locality local in + let local = enforce_module_locality atts.locality in Metasyntax.add_syntactic_definition (Global.env()) (snd lid) x local y let vernac_declare_implicits ~atts r l = @@ -1958,27 +1958,29 @@ let interp ?proof ~atts ~st c = | VernacLocal _ -> assert false (* Syntax *) - | VernacSyntaxExtension (infix, local,sl) -> - vernac_syntax_extension atts local infix sl + | VernacSyntaxExtension (infix, sl) -> + vernac_syntax_extension atts infix sl | VernacDelimiters (sc,lr) -> vernac_delimiters sc lr | VernacBindScope (sc,rl) -> vernac_bind_scope sc rl - | VernacOpenCloseScope (local, s) -> vernac_open_close_scope ~atts local s + | VernacOpenCloseScope (b, s) -> vernac_open_close_scope ~atts (b,s) | VernacArgumentsScope (qid,scl) -> vernac_arguments_scope ~atts qid scl - | VernacInfix (local,mv,qid,sc) -> vernac_infix ~atts local mv qid sc - | VernacNotation (local,c,infpl,sc) -> - vernac_notation ~atts local c infpl sc + | VernacInfix (mv,qid,sc) -> vernac_infix ~atts mv qid sc + | VernacNotation (c,infpl,sc) -> + vernac_notation ~atts c infpl sc | VernacNotationAddFormat(n,k,v) -> Metasyntax.add_notation_extra_printing_rule n k v (* Gallina *) - | VernacDefinition (k,lid,d) -> vernac_definition ~atts k lid d + | VernacDefinition ((discharge,kind),lid,d) -> + vernac_definition ~atts discharge kind lid d | VernacStartTheoremProof (k,l) -> vernac_start_proof ~atts k l | VernacEndProof e -> vernac_end_proof ?proof e | VernacExactProof c -> vernac_exact_proof c - | VernacAssumption (stre,nl,l) -> vernac_assumption ~atts stre l nl + | VernacAssumption ((discharge,kind),nl,l) -> + vernac_assumption ~atts discharge kind l nl | VernacInductive (cum, priv,finite,l) -> vernac_inductive ~atts cum priv finite l - | VernacFixpoint (local, l) -> vernac_fixpoint ~atts local l - | VernacCoFixpoint (local, l) -> vernac_cofixpoint ~atts local l + | VernacFixpoint (discharge, l) -> vernac_fixpoint ~atts discharge l + | VernacCoFixpoint (discharge, l) -> vernac_cofixpoint ~atts discharge l | VernacScheme l -> vernac_scheme l | VernacCombinedScheme (id, l) -> vernac_combined_scheme id l | VernacUniverse l -> vernac_universe ~atts l @@ -2003,9 +2005,9 @@ let interp ?proof ~atts ~st c = | VernacRequire (from, export, qidl) -> vernac_require from export qidl | VernacImport (export,qidl) -> vernac_import export qidl | VernacCanonical qid -> vernac_canonical qid - | VernacCoercion (local,r,s,t) -> vernac_coercion ~atts local r s t - | VernacIdentityCoercion (local,(_,id),s,t) -> - vernac_identity_coercion ~atts local id s t + | VernacCoercion (r,s,t) -> vernac_coercion ~atts r s t + | VernacIdentityCoercion ((_,id),s,t) -> + vernac_identity_coercion ~atts id s t (* Type classes *) | VernacInstance (abst, sup, inst, props, info) -> @@ -2031,10 +2033,10 @@ let interp ?proof ~atts ~st c = (* Commands *) | VernacCreateHintDb (dbname,b) -> vernac_create_hintdb ~atts dbname b | VernacRemoveHints (dbnames,ids) -> vernac_remove_hints ~atts dbnames ids - | VernacHints (local,dbnames,hints) -> - vernac_hints ~atts local dbnames hints - | VernacSyntacticDefinition (id,c,local,b) -> - vernac_syntactic_definition ~atts id c local b + | VernacHints (dbnames,hints) -> + vernac_hints ~atts dbnames hints + | VernacSyntacticDefinition (id,c,b) -> + vernac_syntactic_definition ~atts id c b | VernacDeclareImplicits (qid,l) -> vernac_declare_implicits ~atts qid l | VernacArguments (qid, args, more_implicits, nargs, flags) -> |