X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=components%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=e4df929d76b6f42e816a174b31fd74aafc965194;hb=36243ef64310a9ea2e51a0295744ab5de7abe055;hp=2e7f1224f795a99b46729613cb5ca816a78161cc;hpb=4c64aae84bbfd12abb64e7af5a640192b5051dc3;p=helm.git

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 2e7f1224f..e4df929d7 100644
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/components/grafite_parser/grafiteDisambiguate.ml
@@ -306,20 +306,16 @@ let disambiguate_tactic
    | GrafiteAst.Thesisbecomes (loc, term) ->
         let metasenv,cic = disambiguate_term context metasenv term in
 	metasenv,GrafiteAst.Thesisbecomes (loc, cic)
-   | GrafiteAst.Let1 (loc, id, term, term1) ->
+   | GrafiteAst.ExistsElim (loc, term, id1, term1, id2, term2) ->
         let metasenv,cic = disambiguate_term context metasenv term in
-	let metasenv,cic'= disambiguate_term context metasenv term1 in
-	metasenv,GrafiteAst.Let1(loc, id, cic, cic')
-   | GrafiteAst.Bywehave (loc, term, term1, id, term2, id1) ->
-        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
+	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
 	let metasenv,cic'= disambiguate_term context metasenv term1 in
 	let metasenv,cic''= disambiguate_term context metasenv term2 in
-	metasenv,GrafiteAst.Bywehave(loc, cic, cic', id, cic'', id1)   
+	metasenv,GrafiteAst.AndElim(loc, cic, id, cic', id1, cic'')   
    | GrafiteAst.Case (loc, id, params) ->
         let metasenv,params' =
 	 List.fold_right
@@ -329,7 +325,7 @@ let disambiguate_tactic
 	  ) params (metasenv,[])
 	in
 	metasenv,GrafiteAst.Case(loc, id, params')   
-   | GrafiteAst.RewritingStep (loc, term1, term2, term3) ->
+   | GrafiteAst.RewritingStep (loc, term1, term2, term3, cont) ->
         let metasenv,cic =
 	 match term1 with
 	    None -> metasenv,None
@@ -343,7 +339,7 @@ let disambiguate_tactic
 	  | Some t -> 
 	     let metasenv,t = disambiguate_term context metasenv t in
 	      metasenv,Some t in
-	metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'')   
+	metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)   
 
 
 let disambiguate_obj lexicon_status ~baseuri metasenv (text,prefix_len,obj) =