inductive type ident optional in mutcase

[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 f5aeb5d840d811704dfcae886cf75a76232d3b48..b992a916c28371a82def85cc21e1ff10eadbf39d 100644 (file)
--- a/helm/ocaml/cic_transformations/cicAst.ml
+++ b/helm/ocaml/cic_transformations/cicAst.ml
@@ -97,7 +97,7 @@ type term =
 
   | Appl of term list
   | Binder of binder_kind * capture_variable * term (* kind, name, body *)
-  | Case of term * string * term option * (case_pattern * term) list
+  | Case of term * string option * term option * (case_pattern * term) list
       (* what to match, inductive type, out type, <pattern,action> list *)
   | LetIn of capture_variable * term * term  (* name, body, where *)
   | LetRec of induction_kind * (capture_variable * term * int) list * term