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

[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 ae4eac52082e91e30f5ad602f230836b162438b3..65371bc67a85f85ee8a29f30901442ad3857f7c8 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -328,16 +328,16 @@ 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
-           None -> metasenv,None
-         | Some t -> 
+           `Auto _ as t -> metasenv,t
+         | `Term t -> 
             let metasenv,t = disambiguate_term context metasenv t in
-             metasenv,Some t in
+             metasenv,`Term t in
        metasenv,GrafiteAst.RewritingStep (loc, cic, cic', cic'', cont)