From 2da7bf6327e1f35321f121de9560604b758f0472 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 10 Apr 2016 02:37:41 +0200
Subject: Removing the ad-hoc tactic_expr type.

This type was actually only used by the debug printer of tactics, and only
for atomic tactics. Furthermore, that type was asymmetric, as the underlying
tacexpr type was set to be glob_tactic, when the semantics would have required
a Val.t type.

Furthermore, this type is absent from every contrib I have seen, which hints
again in favour of its lack of meaning.
---
 printing/ppannotation.ml | 2 --
 1 file changed, 2 deletions(-)

(limited to 'printing/ppannotation.ml')

diff --git a/printing/ppannotation.ml b/printing/ppannotation.ml
index df7f925b73..511f93569c 100644
--- a/printing/ppannotation.ml
+++ b/printing/ppannotation.ml
@@ -20,7 +20,6 @@ type t =
   | AGlobAtomicTacticExpr of glob_atomic_tactic_expr
   | ARawTacticExpr        of raw_tactic_expr
   | ARawAtomicTacticExpr  of raw_atomic_tactic_expr
-  | ATacticExpr           of tactic_expr
   | AAtomicTacticExpr     of atomic_tactic_expr
 
 let tag_of_annotation = function
@@ -32,7 +31,6 @@ let tag_of_annotation = function
   | AGlobAtomicTacticExpr _ -> "glob_atomic_tactic_expr"
   | ARawTacticExpr _        -> "raw_tactic_expr"
   | ARawAtomicTacticExpr _  -> "raw_atomic_tactic_expr"
-  | ATacticExpr _           -> "tactic_expr"
   | AAtomicTacticExpr _     -> "atomic_tactic_expr"
 
 let attributes_of_annotation a =
-- 
cgit v1.2.3