X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAst.mli;h=7815a17654e757d1df3bd505345b4d587bc7b1dd;hb=a3acd934eba07f24937e59c3c7a41db82d901025;hp=8abd4f3c9d571e36624cb62136cfec18b800e9a7;hpb=29d132244b797aaaa79319d81e0be4edf05ba7ae;p=helm.git diff --git a/helm/ocaml/cic_transformations/cicAst.mli b/helm/ocaml/cic_transformations/cicAst.mli index 8abd4f3c9..7815a1765 100644 --- a/helm/ocaml/cic_transformations/cicAst.mli +++ b/helm/ocaml/cic_transformations/cicAst.mli @@ -26,6 +26,7 @@ (** {2 Parsing related types} *) type location = Lexing.position * Lexing.position +val pp_location: location -> string (** maps old style (i.e. <= 3.07) lexer location to new style location, * padding with dummy values where needed *) @@ -50,7 +51,6 @@ type term_attribute = type term = | AttributedTerm of term_attribute * term - | Appl of term list | Binder of binder_kind * capture_variable * term (* kind, name, body *) | Case of term * string option * term option * (case_pattern * term) list @@ -77,6 +77,7 @@ and meta_subst = term option and subst = string * term and case_pattern = string * capture_variable list +(* val pack: term list -> term val unpack: term -> term list - +*)