From 6651f223752c9dfbe768273a09a7a4e67c2a5bfd Mon Sep 17 00:00:00 2001 From: clrenard Date: Mon, 3 Sep 2001 10:02:45 +0000 Subject: Correction d'un bug de pretty-print. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1919 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/Inv.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tactics/Inv.v b/tactics/Inv.v index 2b9271aca..4f17f081b 100644 --- a/tactics/Inv.v +++ b/tactics/Inv.v @@ -13,7 +13,7 @@ Require Export Equality. Declare ML Module "Inv" "Leminv". Syntax tactic level 0: - inversion [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id] +| inversion [<<(Inv $ic $id)>>] -> [ (INVCOM $ic) [1 1] $id] | inversion_in [<<(InvIn $ic $id ($LIST $l))>>] -> [ (INVCOM $ic) [1 1] $id (CLAUSE ($LIST $l))] @@ -28,9 +28,9 @@ Syntax tactic level 0: | inv_using_in [<<(UseInversionLemmaIn $id $c ($LIST $l))>>] -> ["Inversion " $id [1 1] "using " $c (CLAUSE ($LIST $l))] -| simple_inv [<<(INVCOM HalfInversion)>>] -> [ "Simple Inversion" ] -| inversion_com [<<(INVCOM Inversion)>>] -> [ "Inversion" ] -| inversion_clear [<<(INVCOM InversionClear)>>] -> [ "Inversion_clear" ]. +| simple_inv [<<(INVCOM "HalfInversion")>>] -> [ "Simple Inversion" ] +| inversion_com [<<(INVCOM "Inversion")>>] -> [ "Inversion" ] +| inversion_clear [<<(INVCOM "InversionClear")>>] -> [ "Inversion_clear" ]. Grammar tactic simple_tactic: ast := -- cgit v1.2.3