]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/cicAst.mli
Bug fixed in check_sort_elimination in the case (not tested so far)
[helm.git] / helm / ocaml / cic_transformations / cicAst.mli
index 8abd4f3c9d571e36624cb62136cfec18b800e9a7..7815a17654e757d1df3bd505345b4d587bc7b1dd 100644 (file)
@@ -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
-
+*)