X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=151ec8a08516cf8074fe6aad4483a662be46d0ff;hb=ec54d490477ece51c19d79750dda9805ffda663c;hp=529353daa3e492e0d7ff12c3bc55795c368731d9;hpb=345d5606c989f46d9de3d3b4c6c53902fabac5bd;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 529353daa..151ec8a08 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -223,12 +223,8 @@ let set_compiled32 f = compiled32 := Some f
 
 let instantiate21 env precedence associativity l1 =
   prerr_endline "instantiate21";
-  let boxify = function
-    | [t] -> t
-    | tl -> Ast.Layout (Ast.Box (Ast.H, tl))
-  in
   let rec subst_singleton env t =
-    boxify (subst env t)
+    CicNotationUtil.boxify (subst env t)
   and subst env = function
     | Ast.AttributedTerm (_, t) -> subst env t
     | Ast.Variable var ->
@@ -264,12 +260,14 @@ let instantiate21 env precedence associativity l1 =
           | [] -> List.rev acc
 	  | value_set :: [] ->
 	      let env = CicNotationEnv.combine rec_decls value_set in
-		instantiate_list ((boxify (subst env p)) :: acc) []
+		instantiate_list
+                  ((CicNotationUtil.boxify (subst env p)) :: acc) []
           | value_set :: tl ->
               let env = CicNotationEnv.combine rec_decls value_set in
-              instantiate_list ((boxify (subst env p @ sep)) :: acc) tl
+              instantiate_list
+                ((CicNotationUtil.boxify (subst env p @ sep)) :: acc) tl
         in
-        instantiate_list [] (List.rev values)
+        instantiate_list [] values
     | Ast.Opt p ->
         let opt_decls = CicNotationEnv.declarations_of_term p in
         let env =