X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=bdf07fb8333f83d8fbecc3084a149d14d9bbc4f6;hb=af73dd5916c5505e8285766f0e3a48a8693943ef;hp=ae447476042d7ea5af675a8fa975f3701d2b4682;hpb=10d33a8c1be31d0c7aeccee8968fd5218ca2510a;p=helm.git

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index ae4474760..bdf07fb83 100644
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -524,8 +524,7 @@ let add_pretty_printer status l2 (CicNotationParser.CL1P (l1,precedence)) =
        level1_patterns21 =
         IntMap.add id l1' status#content_pres_db.level1_patterns21;
        pattern21_matrix = (l2',id)::status#content_pres_db.pattern21_matrix } in
-  let status = load_patterns21 status status#content_pres_db.pattern21_matrix in
-   status,id
+  load_patterns21 status status#content_pres_db.pattern21_matrix 
 
   (* presentation -> content *)
 
@@ -586,7 +585,6 @@ let instantiate_level2 env term =
       new_name
   in
   let rec aux env term =
-(*    prerr_endline ("ENV " ^ NotationPp.pp_env env); *)
     match term with
     | Ast.AttributedTerm (a, term) -> (*Ast.AttributedTerm (a, *)aux env term
     | Ast.Appl terms -> Ast.Appl (List.map (aux env) terms)
@@ -638,7 +636,10 @@ let instantiate_level2 env term =
   and aux_meta_substs env meta_substs = List.map (aux_opt env) meta_substs
   and aux_variable env = function
     | Ast.NumVar name -> Ast.Num (Env.lookup_num env name, 0)
-    | Ast.IdentVar name -> Ast.Ident (Env.lookup_string env name, None)
+    | Ast.IdentVar name ->
+       (match Env.lookup_string env name with
+           Env.Ident x -> Ast.Ident (x, None)
+         | Env.Var x -> Ast.Variable (Ast.IdentVar x))
     | Ast.TermVar (name,(Ast.Level l|Ast.Self l)) -> 
         Ast.AttributedTerm (`Level l,Env.lookup_term env name)
     | Ast.FreshVar name -> Ast.Ident (lookup_fresh_name name, None)