X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_notation%2FcicNotationRew.ml;h=6340d88a15db67f3dddc364540bfddfb702dac02;hb=ed7711935c7377ea8785a9f3b85984785b92030e;hp=3d684fe39b0ff27f57fd3eb6cd23180d30042f20;hpb=cfda0acfce3f5e0b843bfe2b7ba7c371e5690db0;p=helm.git

diff --git a/helm/ocaml/cic_notation/cicNotationRew.ml b/helm/ocaml/cic_notation/cicNotationRew.ml
index 3d684fe39..6340d88a1 100644
--- a/helm/ocaml/cic_notation/cicNotationRew.ml
+++ b/helm/ocaml/cic_notation/cicNotationRew.ml
@@ -116,7 +116,7 @@ let string_of_sort_kind = function
   | `Prop -> "Prop"
   | `Set -> "Set"
   | `CProp -> "CProp"
-  | `Type -> "Type"
+  | `Type _ -> "Type"
 
 let pp_ast0 t k =
   let rec aux =
@@ -275,7 +275,7 @@ let ast_of_acic0 term_info acic k =
       Hashtbl.find term_info.sort id
     with Not_found ->
       prerr_endline (sprintf "warning: sort of id %s not found, using Type" id);
-      `Type
+      `Type (CicUniv.fresh ())
   in
   let aux_substs substs =
     Some
@@ -298,13 +298,13 @@ 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 _) -> idref id (Ast.Sort `Type)
+    | 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) ->
         let binder_kind =
           match sort_of_id id with
-          | `Set | `Type -> `Pi
+          | `Set | `Type _ -> `Pi
           | `Prop | `CProp -> `Forall
         in
         idref id (Ast.Binder (binder_kind,
@@ -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