Empty Box.Text changed to Box.smallskip.

[helm.git] / helm / ocaml / cic_transformations / cicAst.ml

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index 9abd07a75836d6c38ff53e65672fce017d1e5544..45fcc8820b446c884d8ee188f76562a20d6f4a76 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -28,11 +28,13 @@ open Printf
 type location = Lexing.position * Lexing.position
 
 let pp_location (loc_begin, loc_end) =
-  sprintf "(%d,%d)-(%d,%d)"
-    loc_begin.Lexing.pos_lnum
-    (loc_begin.Lexing.pos_cnum - loc_begin.Lexing.pos_bol)
-    loc_end.Lexing.pos_lnum
-    (loc_end.Lexing.pos_cnum - loc_end.Lexing.pos_bol)
+  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 =
@@ -63,6 +65,7 @@ type term =
   | Appl of term list
   | Binder of binder_kind * capture_variable * term
   | Case of term * string option * term option * (case_pattern * term) list
+  | Cast of term * term
   | LetIn of capture_variable * term * term
   | LetRec of induction_kind * (capture_variable * term * int) list * term
   | Ident of string * subst list option
@@ -80,6 +83,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))
@@ -89,4 +93,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
-
+*)