]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/ocaml/cic_transformations/cicAst.ml
merged cic_notation with disambiguation: good luck!
[helm.git] / helm / ocaml / cic_transformations / cicAst.ml
index 3f14ebf7378a9502c07a263feb85b94ccae6471b..45fcc8820b446c884d8ee188f76562a20d6f4a76 100644 (file)
@@ -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