From 20641795624dbb03da0401e4dc503660e5e73df6 Mon Sep 17 00:00:00 2001
From: Matej Kosik
Date: Wed, 16 Dec 2015 15:50:40 +0100
Subject: CLEANUP: Vernacexpr.VernacDeclareTacticDefinition

The definition of Vernacexpr.VernacDeclareTacticDefinition was changed.

The original definition allowed us to represent non-sensical value such as:

  VernacDeclareTacticDefinition(Qualid ..., false, ...)

The new definition prevents that.
---
 intf/vernacexpr.mli | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli
index 0e659459e9..07a206b53e 100644
--- a/intf/vernacexpr.mli
+++ b/intf/vernacexpr.mli
@@ -386,7 +386,7 @@ type vernac_expr =
   | VernacBackTo of int
 
   (* Commands *)
-  | VernacDeclareTacticDefinition of (reference * bool * raw_tactic_expr) list
+  | VernacDeclareTacticDefinition of tacdef_body list
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * reference list
   | VernacHints of obsolete_locality * string list * hints_expr
@@ -453,6 +453,10 @@ type vernac_expr =
   | VernacPolymorphic of bool * vernac_expr
   | VernacLocal of bool * vernac_expr
 
+and tacdef_body =
+  | TacticDefinition of Id.t Loc.located * raw_tactic_expr  (* indicates that user employed ':=' in Ltac body *)
+  | TacticRedefinition of reference * raw_tactic_expr       (* indicates that user employed '::=' in Ltac body *)
+
 and located_vernac_expr = Loc.t * vernac_expr
 
 (* A vernac classifier has to tell if a command:
-- 
cgit v1.2.3