X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationFwd.ml;h=8e955c0b10a8d562647833d501477c3aa87a28ff;hb=ba2dfe6409e95bf9e558dc0d4be382b068671409;hp=b200de2efdfc6de6429523c4f3aa83e6ee1d8443;hpb=724827ba7e5c1419229382487bed53f7dbb862db;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index b200de2ef..8e955c0b1 100644
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -26,7 +26,9 @@
 open CicNotationEnv
 open CicNotationPt
 
-let meta_names_of term =
+(* XXX ZACK: switched to CicNotationUtil.names_of_term, commented code below to
+ * be removes as soon as we believe implementation are equivalent *)
+(* let meta_names_of term =
   let rec names = ref [] in
   let add_name n =
     if List.mem n !names then ()
@@ -90,7 +92,7 @@ let meta_names_of term =
     | _ -> assert false
   in
   aux term ;
-  !names
+  !names *)
 
 let unopt_names names env =
   let rec aux acc = function
@@ -188,7 +190,7 @@ let instantiate_level2 env term =
     | Ascription (term, name) -> assert false
   and aux_magic env = function
     | Default (some_pattern, none_pattern) ->
-        (match meta_names_of some_pattern with
+        (match CicNotationUtil.names_of_term some_pattern with
         | [] -> assert false (* some pattern must contain at least 1 name *)
         | (name :: _) as names ->
             (match lookup_value env name with
@@ -202,13 +204,13 @@ let instantiate_level2 env term =
     | Fold (`Left, base_pattern, names, rec_pattern) ->
         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
         let meta_names =
-          List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+          List.filter ((<>) acc_name)
+            (CicNotationUtil.names_of_term rec_pattern)
         in
         (match meta_names with
         | [] -> 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 
@@ -222,13 +224,13 @@ let instantiate_level2 env term =
     | Fold (`Right, base_pattern, names, rec_pattern) ->
         let acc_name = List.hd names in (* names can't be empty, cfr. parser *)
         let meta_names =
-          List.filter ((<>) acc_name) (meta_names_of rec_pattern)
+          List.filter ((<>) acc_name)
+            (CicNotationUtil.names_of_term rec_pattern)
         in
         (match meta_names with
         | [] -> 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
@@ -238,6 +240,8 @@ let instantiate_level2 env term =
               | _ -> assert false
             in
             instantiate_fold_right env)
+    | If (_, p_true, p_false) as t -> aux env (CicNotationUtil.find_branch (Magic t))
+    | Fail -> assert false
     | _ -> assert false
   in
   aux env term