- decompose tactic: decomposable constants are now allowed (they are unfolded)

[helm.git] / helm / software / components / grafite_engine / grafiteEngine.ml

diff --git a/helm/software/components/grafite_engine/grafiteEngine.ml b/helm/software/components/grafite_engine/grafiteEngine.ml
index df01f8467f2778dbf3a33db297830116dcd0c02b..f95829797a3c91ea75be791f83fac86d0f16ab03 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -79,7 +79,7 @@ let tactic_of_ast status ast =
      Tactics.cut ~mk_fresh_name_callback:(namer_of names) term
   | GrafiteAst.Decompose (_, types, what, names) -> 
       let to_type = function
-         | GrafiteAst.Type (uri, typeno) -> uri, typeno
+         | GrafiteAst.Type (uri, typeno) -> uri, Some typeno
         | GrafiteAst.Ident _            -> assert false
       in
       let user_types = List.rev_map to_type types in