X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=cc8360c28f51d0728996cdb37c7851e11cd69965;hb=c0a733b932a64804f67ac93f9ab9f52bd0614fc6;hp=0c64bbb0794ece3e80c68de116ce640dfbfde413;hpb=cea3a50f515d1e39467073d2b447a9ddfa1a4852;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 0c64bbb07..cc8360c28 100644
--- 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