From f1485f680813df1444c877b37b8eb8dc9c644179 Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 23 Sep 2005 13:16:34 +0000
Subject: [PATCH] avoid pattern matching on attributed terms since this loses
 attributes

---
 helm/ocaml/cic_notation/cicNotationRew.ml | 27 +++++++++++++----------
 1 file changed, 15 insertions(+), 12 deletions(-)

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 0029e3db5..6340d88a1 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -298,7 +298,7 @@ let ast_of_acic0 term_info acic k =
     | Cic.AMeta (id,n,l) -> idref id (Ast.Meta (n, aux_context l))
     | Cic.ASort (id,Cic.Prop) -> idref id (Ast.Sort `Prop)
     | Cic.ASort (id,Cic.Set) -> idref id (Ast.Sort `Set)
-    | Cic.ASort (id,Cic.Type u) ->idref id (Ast.Sort (`Type u))
+    | Cic.ASort (id,Cic.Type u) -> idref id (Ast.Sort (`Type u))
     | Cic.ASort (id,Cic.CProp) -> idref id (Ast.Sort `CProp)
     | Cic.AImplicit _ -> assert false
     | Cic.AProd (id,n,s,t) ->
@@ -418,11 +418,11 @@ let get_compiled32 () =
 let set_compiled21 f = compiled21 := Some f
 let set_compiled32 f = compiled32 := Some f
 
-let instantiate21 env (* precedence associativity *) l1 =
+let instantiate21 env l1 =
   let rec subst_singleton env t =
     CicNotationUtil.group (subst env t)
   and subst env = function
-    | Ast.AttributedTerm (_, t) -> subst env t
+    | Ast.AttributedTerm (attr, t) -> subst env t
     | Ast.Variable var ->
         let name, expected_ty = CicNotationEnv.declaration_of_var var in
         let ty, value =
@@ -508,15 +508,18 @@ let rec pp_ast1 term =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
   in
 (* prerr_endline ("pattern matching from 2 to 1 on term " ^ CicNotationPp.pp_term term); *)
-  (match (get_compiled21 ()) term with
-  | None -> pp_ast0 term pp_ast1
-  | Some (env, pid) ->
-      let prec, assoc, l1 =
-        try
-          Hashtbl.find level1_patterns21 pid
-        with Not_found -> assert false
-      in
-      add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
+  match term with
+  | Ast.AttributedTerm (attrs, term) -> Ast.AttributedTerm (attrs, pp_ast1 term)
+  | _ ->
+      (match (get_compiled21 ()) term with
+      | None -> pp_ast0 term pp_ast1
+      | Some (env, pid) ->
+          let prec, assoc, l1 =
+            try
+              Hashtbl.find level1_patterns21 pid
+            with Not_found -> assert false
+          in
+          add_level_info prec assoc (instantiate21 (ast_env_of_env env) l1))
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function
-- 
2.39.2