new signature of auto_tac, with a new optional argument "full", to invoke the

[helm.git] / helm / ocaml / cic_notation / grafiteParser.ml

diff --git a/helm/ocaml/cic_notation/grafiteParser.ml b/helm/ocaml/cic_notation/grafiteParser.ml
index 5caba868b1e220b2392f337f17e56317baaa2d2f..c3a4b7f01ef998e30c5debd31d5ee34a032725bb 100644 (file)
--- a/helm/ocaml/cic_notation/grafiteParser.ml
+++ b/helm/ocaml/cic_notation/grafiteParser.ml
@@ -112,8 +112,9 @@ EXTEND
     | IDENT "auto";
       depth = OPT [ IDENT "depth"; SYMBOL "="; i = int -> i ];
       width = OPT [ IDENT "width"; SYMBOL "="; i = int -> i ];
-      paramodulation = OPT [ IDENT "paramodulation" ] ->  (* ALB *)
-          GrafiteAst.Auto (loc,depth,width,paramodulation)
+      paramodulation = OPT [ IDENT "paramodulation" ];
+      full = OPT [ IDENT "full" ] ->  (* ALB *)
+          GrafiteAst.Auto (loc,depth,width,paramodulation,full)
     | IDENT "clear"; id = IDENT ->
         GrafiteAst.Clear (loc,id)
     | IDENT "clearbody"; id = IDENT ->