removed no longer used METAs

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

diff --git a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
index da72944781d5f0138b286fde5529d1778e88e40d..f5ea66f2f6883e06a840744579277817577fe32f 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+(* $Id$ *)
+
 exception BaseUriNotSetYet
 
 let singleton = function
@@ -79,6 +81,7 @@ let disambiguate_reduction_kind lexicon_status_ref = function
   | `Unfold (Some t) ->
       let t = disambiguate_lazy_term lexicon_status_ref t in
       `Unfold (Some t)
+  | `Demodulate
   | `Normalize
   | `Reduce
   | `Simpl
@@ -246,7 +249,7 @@ let disambiguate_obj lexicon_status ~baseuri metasenv obj =
   lexicon_status, metasenv, cic
   
 let disambiguate_command lexicon_status ~baseuri metasenv =
-  function
+ function
   | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
@@ -258,3 +261,29 @@ let disambiguate_command lexicon_status ~baseuri metasenv =
       let lexicon_status,metasenv,obj =
        disambiguate_obj lexicon_status ~baseuri metasenv obj in
       lexicon_status, metasenv, GrafiteAst.Obj (loc,obj)
+
+let disambiguate_macro lexicon_status_ref metasenv context macro =
+ let disambiguate_term = disambiguate_term lexicon_status_ref in
+  match macro with
+   | GrafiteAst.WMatch (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WMatch (loc,term)
+   | GrafiteAst.WInstance (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WInstance (loc,term)
+   | GrafiteAst.WElim (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WElim (loc,term)
+   | GrafiteAst.WHint (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.WHint (loc,term)
+   | GrafiteAst.Check (loc,term) ->
+      let metasenv,term = disambiguate_term context metasenv term in
+       metasenv,GrafiteAst.Check (loc,term)
+   | GrafiteAst.Hint _
+   | GrafiteAst.WLocate _ as macro ->
+      metasenv,macro
+   | GrafiteAst.Quit _
+   | GrafiteAst.Print _
+   | GrafiteAst.Search_pat _
+   | GrafiteAst.Search_term _ -> assert false