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 7b4e6157b70fd43950da32b8d8f832628cbcffa5..2a5d3c0b0777fe500bef007004befa0e436167c4 100644 (file)
--- 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)