X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fgrafite%2FgrafiteAst.ml;h=8979129158b34bcd8a9ffa03577dca64bfb399e9;hb=5d010a40c726d9a7eceeb35e70e41a158eb63c70;hp=9c5d56024917795facba7653bc89d1019a192754;hpb=36014ac060f150e7d93f607c914a0b06239715c0;p=helm.git diff --git a/helm/software/components/grafite/grafiteAst.ml b/helm/software/components/grafite/grafiteAst.ml index 9c5d56024..897912915 100644 --- a/helm/software/components/grafite/grafiteAst.ml +++ b/helm/software/components/grafite/grafiteAst.ml @@ -106,6 +106,9 @@ type search_kind = [ `Locate | `Hint | `Match | `Elim ] type print_kind = [ `Env | `Coer ] +type style = Declarative + | Procedural + type 'term macro = (* Whelp's stuff *) | WHint of loc * 'term @@ -116,7 +119,7 @@ type 'term macro = (* real macros *) | Check of loc * 'term | Hint of loc - | Inline of loc * string * string (* URI or base-uri, name prefix *) + | Inline of loc * style * string * string (* URI or base-uri, name prefix *) (** To be increased each time the command type below changes, used for "safe" * marshalling *)