* implemented unless

[helm.git] / helm / ocaml / cic_notation / cicNotationPt.ml

diff --git a/helm/ocaml/cic_notation/cicNotationPt.ml b/helm/ocaml/cic_notation/cicNotationPt.ml
index 0a5a1285331c9210d9e99bcb53018e7c0d7ec9b2..56bf8547441bd218ee6fd393569902c558942cfe 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -117,7 +117,8 @@ and magic_term =
   | Fold of fold_kind * term * string list * term
     (* base case pattern, recursive case bound names, recursive case pattern *)
   | Default of term * term  (* "some" case pattern, "none" case pattern *)
-  | If of term * term (* guard, pattern *)
+  | If of term * term (* guard, body *)
+  | Unless of term * term (* guard, body *)
 
 and pattern_variable =
   (* level 1 and 2 variables *)