avoid pattern matching on attributed terms since this loses attributes

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 0029e3db5570f95b2015211869e817257339ee20..6340d88a15db67f3dddc364540bfddfb702dac02 100644 (file)
--- 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