Debugging code removed.

[helm.git] / matita / components / content_pres / termContentPres.ml

diff --git a/matita/components/content_pres/termContentPres.ml b/matita/components/content_pres/termContentPres.ml
index 6b0d9d0c8595c4ade106306369efb9acc20e9389..bdf07fb8333f83d8fbecc3084a149d14d9bbc4f6 100644 (file)
--- a/matita/components/content_pres/termContentPres.ml
+++ b/matita/components/content_pres/termContentPres.ml
@@ -585,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)
@@ -637,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)