X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Focaml%2Fcic_notation%2FcicNotationFwd.ml;h=93a4c684d019de589035215efcb4506c474da3db;hb=0c04e1f673d69ac652c15705863931c45e107515;hp=f2e2c7164efa6244d045a073eb1331f13877a8ba;hpb=26cce624c98e795521078794c748758798031704;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationFwd.ml b/helm/ocaml/cic_notation/cicNotationFwd.ml
index f2e2c7164..93a4c684d 100644
--- a/helm/ocaml/cic_notation/cicNotationFwd.ml
+++ b/helm/ocaml/cic_notation/cicNotationFwd.ml
@@ -23,6 +23,8 @@
  * http://helm.cs.unibo.it/
  *)
 
+open Printf
+
 open CicNotationEnv
 open CicNotationPt
 
@@ -211,7 +213,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 +233,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,9 +242,24 @@ 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
 
+let instantiate_appl_pattern env appl_pattern =
+  let lookup name =
+    try List.assoc name env
+    with Not_found ->
+      prerr_endline (sprintf "Name %s not found" name);
+      assert false
+  in
+  let rec aux = function
+    | UriPattern uri -> CicUtil.term_of_uri uri
+    | ImplicitPattern -> Cic.Implicit None
+    | VarPattern name -> lookup name
+    | ApplPattern terms -> Cic.Appl (List.map aux terms)
+  in
+  aux appl_pattern
+