* various bug fix related to the environment returned when a match

[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 ab484c3eb76a4db2e39d217cbe5b2731fb413c6c..0a5a1285331c9210d9e99bcb53018e7c0d7ec9b2 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationPt.ml
+++ b/helm/ocaml/cic_notation/cicNotationPt.ml
@@ -109,14 +109,15 @@ and layout_pattern =
 
 and magic_term =
   (* level 1 magics *)
-  | List0 of term * literal option
-  | List1 of term * literal option
+  | List0 of term * literal option (* pattern, separator *)
+  | List1 of term * literal option (* pattern, separator *)
   | Opt of term
 
   (* level 2 magics *)
   | 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 *)
 
 and pattern_variable =
   (* level 1 and 2 variables *)