trace generation with "// by _;"

[helm.git] / helm / software / components / grafite / grafiteAst.ml

diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml
index 5b10a5465cc5fc9ad68889fc87a8236ad3bede2c..97dbb04868ebf2c76ebdbd55b491f6c5403aed8e 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -200,6 +200,7 @@ type ('term,'lazy_term) macro =
 type nmacro =
   | NCheck of loc * CicNotationPt.term
   | Screenshot of loc * string
+  | NAutoInteractive of loc * CicNotationPt.term auto_params
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)