X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_transformations%2FcicAst.ml;h=45fcc8820b446c884d8ee188f76562a20d6f4a76;hb=1bcad789810fd37d346e690f18557aeedc6fe08c;hp=ca48567863aa8d9c88ebf6eba9aa986db55c1fae;hpb=51d9b14ac63f4d4f045772ccd006b49e87d8f4bc;p=helm.git

diff --git a/helm/ocaml/cic_transformations/cicAst.ml b/helm/ocaml/cic_transformations/cicAst.ml
index ca4856786..45fcc8820 100644
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -65,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
@@ -82,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))
@@ -91,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
-
+*)