snapshot (minor changes)

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

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 529353daa3e492e0d7ff12c3bc55795c368731d9..151ec8a08516cf8074fe6aad4483a662be46d0ff 100644 (file)
--- 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 =