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.
coq · Nov 23, 2017 · dd65bb5 · dd65bb5
1 parent 22ae762
commit dd65bb5
Show file tree

Hide file tree

Showing 16 changed files with 203 additions and 278 deletions.
diff --git a/API/API.mli b/API/API.mli
@@ -1167,6 +1167,10 @@ sig
     | CoFinite
     | BiFinite
 
+  type discharge =
+    | DoDischarge
+    | NoDischarge
+
   type locality =
     | Discharge
     | Local
@@ -1185,6 +1189,7 @@ sig
     | IdentityCoercion
     | Instance
     | Method
+    | Let
   type theorem_kind =
     | Theorem
     | Lemma
@@ -3880,8 +3885,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
@@ -3996,29 +3999,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
@@ -4029,9 +4030,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
@@ -4065,9 +4066,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
@@ -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
@@ -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
@@ -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
@@ -149,10 +149,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
@@ -325,31 +321,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
@@ -362,10 +354,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 *)
@@ -416,9 +407,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
@@ -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
@@ -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
@@ -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 ] ]