aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2017-09-12 17:26:53 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2017-11-29 16:12:14 +0100
commitae5944b360c1e181fa162d7d6dced7e671c6fbe6 (patch)
treeca5f2c680d0cd33028e75a579d5ffca31e83d6b0
parentb23df225c7df7883af6ecfa921986cfb6fd3cd7c (diff)
Remove "obsolete_locality" and fix STM vernac classification.
We remove deprecated syntax "Coercion Local" and such, and seize the opportunity to refactor some code around vernac_expr. We also do a small fix on the STM classification, which didn't know about Let Fixpoint and Let CoFixpoint. This is a preliminary step for the work on attributes.
-rw-r--r--API/API.mli33
-rw-r--r--CHANGES4
-rw-r--r--interp/dumpglob.ml2
-rw-r--r--intf/decl_kinds.ml3
-rw-r--r--intf/vernacexpr.ml33
-rw-r--r--library/kindops.ml48
-rw-r--r--library/kindops.mli2
-rw-r--r--parsing/g_proofs.ml49
-rw-r--r--parsing/g_vernac.ml490
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/ssr/ssrvernac.ml46
-rw-r--r--printing/ppvernac.ml64
-rw-r--r--stm/vernac_classifier.ml21
-rw-r--r--vernac/locality.ml57
-rw-r--r--vernac/locality.mli13
-rw-r--r--vernac/vernacentries.ml92
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 *
diff --git a/CHANGES b/CHANGES
index 7a326c589..6a7a5a42b 100644
--- a/CHANGES
+++ b/CHANGES
@@ -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) ->