X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matitaB%2Fcomponents%2Fcontent_pres%2FtermContentPres.ml;h=53f0265b7ffff0a33d10cd5974bf4e9e9feef558;hb=6d4277977478ef9bcadaffbef3d4bb04ac0250a5;hp=7473838ca5e6b6424e36017dc08b1c28cebe7c09;hpb=98f0fac6d03367be776303e7ba353b75878aaa40;p=helm.git

diff --git a/matitaB/components/content_pres/termContentPres.ml b/matitaB/components/content_pres/termContentPres.ml
index 7473838ca..53f0265b7 100644
--- a/matitaB/components/content_pres/termContentPres.ml
+++ b/matitaB/components/content_pres/termContentPres.ml
@@ -467,6 +467,7 @@ let rec pp_ast1 status term =
         NotationEnv.OptValue (Some (pp_value v))
     | NotationEnv.ListValue vl ->
         NotationEnv.ListValue (List.map pp_value vl)
+    | NotationEnv.LocValue _ as v -> v
   in
   let ast_env_of_env env =
     List.map (fun (var, (ty, value)) -> (var, (ty, pp_value value))) env
@@ -574,7 +575,7 @@ let tail_names names env =
   in
   aux [] env
 
-let instantiate_level2 status env term =
+let instantiate_level2 status env loc term =
 (*   prerr_endline ("istanzio: " ^ NotationPp.pp_term term); *)
   let fresh_env = ref [] in
   let lookup_fresh_name n =
@@ -605,8 +606,8 @@ let instantiate_level2 status env term =
     | Ast.Ident _
     | Ast.Num _
     | Ast.Sort _
-    | Ast.Symbol _
     | Ast.UserInput -> term
+    | Ast.Symbol _ -> Ast.AttributedTerm (`Loc loc, term)
 
     | Ast.Magic magic -> aux_magic env magic
     | Ast.Variable var -> aux_variable env var