* implemented unless

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

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index 10bab9e36fb3bcaedd333aec34ec64610077164d..f2e2c7164efa6244d045a073eb1331f13877a8ba 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -242,6 +242,8 @@ let instantiate_level2 env term =
               | _ -> assert false
             in
             instantiate_fold_right env)
+    | If (_, body)
+    | Unless (_, body) -> aux env body
     | _ -> assert false
   in
   aux env term