From bde36d4b00185065628324d8ca71994f84eae244 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 12 Apr 2016 22:25:26 +0200
Subject: In the short term, stronger invariant on the syntax of TacAssert,
 what allows for a simpler re-printing of assert.

Also fixing the precedence for printing "by" clause.
---
 intf/tacexpr.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'intf')

diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index e06436d8a3..f6b60b2d58 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -148,7 +148,7 @@ type 'a gen_atomic_tactic_expr =
   | TacMutualFix of Id.t * int * (Id.t * int * 'trm) list
   | TacMutualCofix of Id.t * (Id.t * 'trm) list
   | TacAssert of
-      bool * 'tacexpr option *
+      bool * 'tacexpr option option *
       'dtrm intro_pattern_expr located option * 'trm
   | TacGeneralize of ('trm with_occurrences * Name.t) list
   | TacLetTac of Name.t * 'trm * 'nam clause_expr * letin_flag *
-- 
cgit v1.2.3