X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAst.ml;h=3f14ebf7378a9502c07a263feb85b94ccae6471b;hb=29a3bd5d160f31873236c93a008a9e4fd31c305e;hp=3991813726766008222b5e08a33227a36117dd99;hpb=29d132244b797aaaa79319d81e0be4edf05ba7ae;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index 399181372..3f14ebf73 100644
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -23,8 +23,19 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 type location = Lexing.position * Lexing.position
 
+let pp_location (loc_begin, loc_end) =
+  let c_begin = loc_begin.Lexing.pos_cnum - loc_begin.Lexing.pos_bol in
+  let c_end = loc_end.Lexing.pos_cnum - loc_end.Lexing.pos_bol in
+  if loc_begin.Lexing.pos_lnum = -1 || loc_end.Lexing.pos_lnum = -1 then
+      sprintf "%d-%d" c_begin c_end
+    else
+      sprintf "(%d,%d)-(%d,%d)" loc_begin.Lexing.pos_lnum c_begin
+        loc_end.Lexing.pos_lnum c_end
+
 let floc_of_loc (loc_begin, loc_end) =
   let floc_begin =
     { Lexing.pos_fname = ""; Lexing.pos_lnum = -1; Lexing.pos_bol = -1;
@@ -71,6 +82,7 @@ and meta_subst = term option
 and subst = string * term
 and case_pattern = string * capture_variable list
 
+(*
 let pack asts =
   List.fold_right
     (fun ast acc -> Binder (`Forall, (Cic.Anonymous, Some ast), acc))
@@ -80,4 +92,4 @@ let rec unpack = function
   | Binder (`Forall, (Cic.Anonymous, Some ast), Sort `Type) -> [ast]
   | Binder (`Forall, (Cic.Anonymous, Some ast), tgt) -> ast :: unpack tgt
   | _ -> assert false
-
+*)