X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fcomponents%2Facic_content%2FcicNotationPt.ml;h=3ffa9525808119fcd64a423bb1251feab46ea294;hb=dee331ab42d5d625f32fecc3e70df013c2dd093d;hp=3c96a5a512ac7d1bd49b94ff9ab79cf373b9d0b9;hpb=266fe24a5a5548c30f597ccd38578877643404d3;p=helm.git diff --git a/helm/software/components/acic_content/cicNotationPt.ml b/helm/software/components/acic_content/cicNotationPt.ml index 3c96a5a51..3ffa95258 100644 --- a/helm/software/components/acic_content/cicNotationPt.ml +++ b/helm/software/components/acic_content/cicNotationPt.ml @@ -62,7 +62,7 @@ type 'term capture_variable = 'term * 'term option (** To be increased each time the term type below changes, used for "safe" * marshalling *) -let magic = 5 +let magic = 6 type term = (* CIC AST *) @@ -122,12 +122,14 @@ and layout_pattern = | InfRule of term * term * term (* | array of term * literal option * literal option |+ column separator, row separator +| *) + | Maction of term list | Sqrt of term | Root of term * term (* argument, index *) | Break | Box of box_spec * term list | Group of term list | Mstyle of (string * string) list * term list + | Mpadded of (string * string) list * term list and magic_term = (* level 1 magics *)