From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 16 Apr 2009 12:27:12 +0000 (+0000)
Subject: The context is now parsed in the reverse (right) order.
X-Git-Tag: make_still_working~4077
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f3e3640298e3edc6920d0c8d665c00f12e134c93;p=helm.git

The context is now parsed in the reverse (right) order.
---

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 7b4e6157b..2a5d3c0b0 100644
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -190,7 +190,7 @@ EXTEND
                         SYMBOL <:unicode<def>> ; bo = tactic_term ->
             id,`Def (bo,ty)];
         SYMBOL <:unicode<vdash>>;
-        concl = tactic_term -> (hyps,concl) ] ->
+        concl = tactic_term -> (List.rev hyps,concl) ] ->
          GrafiteAst.NAssert (loc, seqs)
     | IDENT "ncases"; what = tactic_term ; where = pattern_spec ->
         GrafiteAst.NCases (loc, what, where)