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 2f95a56350f5af1b5fa492c36d2310fa18debb18..3af28fddde636d25a41d279d923a7ee8e334b010 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -29,6 +29,9 @@ type pattern_id = int
 type interpretation_id = pattern_id
 type pretty_printer_id = pattern_id
 
+let default_prec = 50
+let default_assoc = Gramext.NonA
+
 type term_info =
   { sort: (Cic.id, CicNotationPt.sort_kind) Hashtbl.t;
     uri: (Cic.id, string) Hashtbl.t;
@@ -252,7 +255,7 @@ 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 (* precedence associativity *) l1 =
   let rec subst_singleton env t =
     CicNotationUtil.boxify (subst env t)
   and subst env = function
@@ -345,7 +348,8 @@ let rec pp_ast1 term =
           Hashtbl.find level1_patterns21 pid
         with Not_found -> assert false
       in
-      instantiate21 (ast_env_of_env env) precedence associativity l1
+      Ast.AttributedTerm (`Level (precedence, associativity),
+        (instantiate21 (ast_env_of_env env) (* precedence associativity *) l1))
 
 let instantiate32 term_info env symbol args =
   let rec instantiate_arg = function
@@ -408,7 +412,9 @@ let add_interpretation (symbol, args) appl_pattern =
   load_patterns32 !pattern32_matrix;
   id
 
-let add_pretty_printer ?precedence ?associativity l2 l1 =
+let add_pretty_printer
+  ?(precedence = default_prec) ?(associativity = default_assoc) l2 l1
+=
   let id = fresh_id () in
   let l2' = CicNotationUtil.strip_attributes l2 in
   Hashtbl.add level1_patterns21 id (precedence, associativity, l1);