constructor accepts the arguments of the constructor...

[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 2a04b7470249205b4e39af535b8bab1a16813d70..7e314670b1106651747ee91f8a18bb5b64e6f5ae 100644 (file)
--- a/helm/software/components/grafite_engine/grafiteEngine.ml
+++ b/helm/software/components/grafite_engine/grafiteEngine.ml
@@ -653,7 +653,9 @@ let eval_ng_tac tac =
   | GrafiteAst.NChange (_loc, pat, ww) -> 
       NTactics.change_tac 
        ~where:(text,prefix_len,pat) ~with_what:(text,prefix_len,ww) 
-  | GrafiteAst.NConstructor (_loc,num) -> NTactics.constructor_tac ?num
+  | GrafiteAst.NConstructor (_loc,num,args) -> 
+     NTactics.constructor_tac 
+       ?num ~args:(List.map (fun x -> text,prefix_len,x) args)
   | GrafiteAst.NDot _ -> NTactics.dot_tac 
   | GrafiteAst.NElim (_loc, what, where) ->
       NTactics.elim_tac