snapshot

[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 f2e2c7164efa6244d045a073eb1331f13877a8ba..8e955c0b10a8d562647833d501477c3aa87a28ff 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -211,7 +211,6 @@ let instantiate_level2 env term =
         | [] -> assert false (* as above *)
         | (name :: _) as names ->
             let rec instantiate_fold_left acc env' =
-              prerr_endline "instantiate_fold_left";
               match lookup_value env' name with
               | ListValue (_ :: _) ->
                   instantiate_fold_left 
@@ -232,7 +231,6 @@ let instantiate_level2 env term =
         | [] -> assert false (* as above *)
         | (name :: _) as names ->
             let rec instantiate_fold_right env' =
-              prerr_endline "instantiate_fold_right";
               match lookup_value env' name with
               | ListValue (_ :: _) ->
                   let acc = instantiate_fold_right (tail_names names env') in
@@ -242,8 +240,8 @@ let instantiate_level2 env term =
               | _ -> assert false
             in
             instantiate_fold_right env)
-    | If (_, body)
-    | Unless (_, body) -> aux env body
+    | If (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t))
+    | Fail -> assert false
     | _ -> assert false
   in
   aux env term