- hExtlib: new function "list_assoc_all"

[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 f6555fa04c7dd5ed86bb8c4f6c6bbe8d7fee4feb..4006320be2a2a58e770e8cf80efdbecce13939db 100644 (file)
--- a/helm/software/components/grafite/grafiteAst.ml
+++ b/helm/software/components/grafite/grafiteAst.ml
@@ -147,8 +147,11 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ]
 
 type print_kind = [ `Env | `Coer ]
 
-type presentation_style = Declarative
-                        | Procedural of int option
+type inline_param = IPPrefix of string
+                  | IPProcedural
+                  | IPDepth of int
+                 | IPAs of Cic.object_flavour
+                  | IPNoDefaults 
 
 type ('term,'lazy_term) macro = 
   (* Whelp's stuff *)
@@ -162,8 +165,8 @@ type ('term,'lazy_term) macro =
   | Check of loc * 'term 
   | Hint of loc * bool
   | AutoInteractive of loc * 'term auto_params
-  | Inline of loc * presentation_style * string * string * Cic.object_flavour option
-     (* URI or base-uri, name prefix, flavour *) 
+  | Inline of loc * string * inline_param list
+     (* URI or base-uri, parameters *) 
 
 (** To be increased each time the command type below changes, used for "safe"
  * marshalling *)