Procedural: 2 bug fix in eta expansion + 1 bug fix in pattern generation

[helm.git] / helm / software / components / grafite_parser / grafiteParser.ml

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index fd757d141a9334ead4539e6c5d74bf0ffc552170..3653c46069adc15ff3a2be2aa7edc7ca9693ea1f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -253,12 +253,12 @@ EXTEND
         | BYC_weproved (ty,id,t1) ->
            GrafiteAst.By_term_we_proved(loc, t', ty, id, t1)
         | BYC_letsuchthat (id1,t1,id2,t2) ->
-           (match t with
+          (* (match t with
                LNone floc ->
                  raise (HExtlib.Localized
                  (floc,CicNotationParser.Parse_error
                    "tactic_term expected here"))
-              | LSome t -> GrafiteAst.ExistsElim (loc, t, id1, t1, id2, t2))
+              | LSome t ->*) GrafiteAst.ExistsElim (loc, t', id1, t1, id2, t2)(*)*)
         | BYC_wehaveand (id1,t1,id2,t2) ->
            (match t with
                LNone floc ->