X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite_parser%2FgrafiteDisambiguate.ml;h=65371bc67a85f85ee8a29f30901442ad3857f7c8;hb=36014ac060f150e7d93f607c914a0b06239715c0;hp=4c2a631761679fb8a01fa808d93af4212cba4bf6;hpb=403b7486e9f2cb5583a2c8035cf419bbac982fb1;p=helm.git

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 4c2a63176..65371bc67 100644
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -328,9 +328,9 @@ let disambiguate_tactic
         let metasenv,cic =
 	 match term1 with
 	    None -> metasenv,None
-	  | Some t -> 
+	  | Some (start,t) -> 
 	     let metasenv,t = disambiguate_term context metasenv t in
-	      metasenv,Some t in
+	      metasenv,Some (start,t) in
 	let metasenv,cic'= disambiguate_term context metasenv term2 in
         let metasenv,cic'' =
 	 match term3 with