New syntax and semantics for the rewriting steps that make the pretty-printed

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

diff --git a/components/grafite_parser/grafiteDisambiguate.ml b/components/grafite_parser/grafiteDisambiguate.ml
index 4c2a631761679fb8a01fa808d93af4212cba4bf6..65371bc67a85f85ee8a29f30901442ad3857f7c8 100644 (file)
--- a/components/grafite_parser/grafiteDisambiguate.ml
+++ b/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