* 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;
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))
| Binder (`Forall, (Cic.Anonymous, Some ast), Sort `Type) -> [ast]
| Binder (`Forall, (Cic.Anonymous, Some ast), tgt) -> ast :: unpack tgt
| _ -> assert false
-
+*)