snapshot

[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 dac2b4c7348b64145a7001f52c908d89eacae13d..207b26a233d139773815234a62843838e115020d 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -118,7 +118,6 @@ let pp_ast0 t k =
   aux t
 
 let ast_of_acic0 term_info acic k =
-(*   prerr_endline "ast_of_acic0"; *)
   let k = k term_info in
   let register_uri id uri = Hashtbl.add term_info.uri id uri in
   let sort_of_id id =
@@ -324,7 +323,8 @@ let instantiate21 env (* precedence associativity *) l1 =
          end
     | _ -> assert false (* impossible *)
   and subst_layout env = function
-    | Ast.Box (kind, tl) -> Ast.Box (kind, List.concat (List.map (subst env) tl))
+    | Ast.Box (kind, tl) ->
+        Ast.Box (kind, List.concat (List.map (subst env) tl))
     | l -> CicNotationUtil.visit_layout (subst_singleton env) l
   in
     subst_singleton env l1
@@ -333,6 +333,7 @@ let rec pp_ast1 term =
   let rec pp_value = function
     | CicNotationEnv.NumValue _ as v -> v
     | CicNotationEnv.StringValue _ as v -> v
+(*     | CicNotationEnv.TermValue t when t == term -> CicNotationEnv.TermValue (pp_ast0 t pp_ast1) *)
     | CicNotationEnv.TermValue t -> CicNotationEnv.TermValue (pp_ast1 t)
     | CicNotationEnv.OptValue None as v -> v
     | CicNotationEnv.OptValue (Some v) -> 
@@ -346,16 +347,18 @@ let rec pp_ast1 term =
   match term with
   | Ast.AttributedTerm (attrs, t) -> Ast.AttributedTerm (attrs, pp_ast1 t)
   | _ ->
-      (match (get_compiled21 ()) term with
-      | None -> pp_ast0 term pp_ast1
-      | Some (env, pid) ->
-          let precedence, associativity, l1 =
-            try
-              Hashtbl.find level1_patterns21 pid
-            with Not_found -> assert false
-          in
-          Ast.AttributedTerm (`Level (precedence, associativity),
-            (instantiate21 (ast_env_of_env env) l1)))
+      begin
+       match (get_compiled21 ()) term with
+         | None -> pp_ast0 term pp_ast1
+         | Some (env, pid) ->
+              let precedence, associativity, l1 =
+               try
+                 Hashtbl.find level1_patterns21 pid
+               with Not_found -> assert false
+              in
+               Ast.AttributedTerm (`Level (precedence, associativity),
+                               (instantiate21 (ast_env_of_env env) l1))
+      end
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function