New tactic: inversion.

[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 9e52f92b17fd2d7382be7e4f07589fbb885ba4e0..e6cc064a5e928ede7333bd4f776378e1abe03c62 100644 (file)
--- a/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/ocaml/grafite_parser/grafiteDisambiguate.ml
@@ -69,7 +69,7 @@ let disambiguate_lazy_term status_ref term =
 
 let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
   let interp path = Disambiguate.interpretate_path [] path in
-  let goal_path = interp goal_path in
+  let goal_path = HExtlib.map_option interp goal_path in
   let hyp_paths = List.map (fun (name, path) -> name, interp path) hyp_paths in
   let wanted =
    match wanted with
@@ -78,7 +78,7 @@ let disambiguate_pattern status_ref (wanted, hyp_paths, goal_path) =
        let wanted = disambiguate_lazy_term status_ref wanted in
        Some wanted
   in
-  (wanted, hyp_paths ,goal_path)
+  (wanted, hyp_paths, goal_path)
 
 let disambiguate_reduction_kind aliases_ref = function
   | `Unfold (Some t) ->
@@ -170,6 +170,9 @@ let disambiguate_tactic status goal tactic =
         let term = disambiguate_term status_ref goal term in
         GrafiteAst.Injection (loc,term)
     | GrafiteAst.Intros (loc, num, names) -> GrafiteAst.Intros (loc, num, names)
+    | GrafiteAst.Inversion (loc, term) ->
+       let term = disambiguate_term status_ref goal term in
+        GrafiteAst.Inversion (loc, term)
     | GrafiteAst.LApply (loc, depth, to_what, what, ident) ->
        let f term to_what =
           let term = disambiguate_term status_ref goal term in
@@ -233,21 +236,18 @@ let disambiguate_obj status obj =
 let disambiguate_command status =
   function
   | GrafiteAst.Alias _
+  | GrafiteAst.Coercion _
   | GrafiteAst.Default _
   | GrafiteAst.Drop _
   | GrafiteAst.Dump _
   | GrafiteAst.Include _
   | GrafiteAst.Interpretation _
-  | GrafiteAst.Metadata _
   | GrafiteAst.Notation _
   | GrafiteAst.Qed _
   | GrafiteAst.Render _
   | GrafiteAst.Set _ as cmd ->
       status,cmd
-  | GrafiteAst.Coercion (loc, term, add_composites) ->
-      let status_ref = ref status in
-      let term = disambiguate_term ~context:[] status_ref ~-1 term in
-      !status_ref, GrafiteAst.Coercion (loc,term,add_composites)
   | GrafiteAst.Obj (loc,obj) ->
       let status,obj = disambiguate_obj status obj in
       status, GrafiteAst.Obj (loc,obj)
+