merged cic_notation with disambiguation: good luck!

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

diff --git a/helm/ocaml/cic_transformations/cicAst.mli b/helm/ocaml/cic_transformations/cicAst.mli
index 7815a17654e757d1df3bd505345b4d587bc7b1dd..97cda2e47d9c5c5dd0723f76859e0619a211c27a 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAst.mli
+++ b/helm/ocaml/cic_transformations/cicAst.mli
@@ -55,6 +55,7 @@ type term =
   | Binder of binder_kind * capture_variable * term (* kind, name, body *)
   | Case of term * string option * term option * (case_pattern * term) list
       (* what to match, inductive type, out type, <pattern,action> list *)
+  | Cast of term * term
   | LetIn of capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (capture_variable * term * int) list * term
       (* (name, body, decreasing argument) list, where *)