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

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

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 0c64bbb0794ece3e80c68de116ce640dfbfde413..cc8360c28f51d0728996cdb37c7851e11cd69965 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -297,9 +297,14 @@ let disambiguate_tactic
         let metasenv,cic = disambiguate_term context metasenv term in
        metasenv,GrafiteAst.Thesisbecomes (loc, cic)
    | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
-        let metasenv,cic = disambiguate_term context metasenv term in
+       let metasenv,cic =
+           match term with
+             None -> metasenv,None
+           | Some t ->
+                 let metasenv,t = disambiguate_term context metasenv t in
+                 metasenv,Some t in
         let metasenv,cic' = disambiguate_term context metasenv term1 in
-       let metasenv,cic''= disambiguate_term context metasenv term2 in
+       let cic''= disambiguate_lazy_term term2 in
        metasenv,GrafiteAst.ExistsElim(loc, cic, id1, cic', id2, cic'')
    | GrafiteAst.AndElim (loc, term, id, term1, id1, term2) ->
        let metasenv,cic = disambiguate_term context metasenv term in