From 69bf012d0d2a71ed19fc89b31073747f85f9a11d Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 23 Oct 2001 22:40:38 +0000
Subject: Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tauto.ml4 | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tauto.ml4 b/tactics/tauto.ml4
index ab96c8759b..7ccca8c758 100644
--- a/tactics/tauto.ml4
+++ b/tactics/tauto.ml4
@@ -60,9 +60,9 @@ let axioms ist =
   and t_is_empty = tacticIn is_empty in
   <:tactic<
     Match Context With
-    |[ |- ?1] -> $t_is_unit;Constructor
-    |[ _:?1 |- ?] -> $t_is_empty
-    |[ _:?1 |- ?1] -> Assumption>>
+    |[|- ?1] -> $t_is_unit;Constructor
+    |[_:?1 |- ?] -> $t_is_empty
+    |[_:?1 |- ?1] -> Assumption>>
 
 let simplif ist =
   let t_is_unit = tacticIn is_unit
-- 
cgit v1.2.3