X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=matitaB%2Fcomponents%2Fng_tactics%2FnCicElim.ml;h=0840b16a65718f6bb77f71dfb2e92b02dadd9e7e;hb=bfafdf7d8313ddd24c06d8ce3bba874f780403a9;hp=24fd7d8e9aa0eb65104e4bc7154632985f1e0d39;hpb=cacbe3c6493ddce76c4c13379ade271d8dd172e8;p=helm.git

diff --git a/matitaB/components/ng_tactics/nCicElim.ml b/matitaB/components/ng_tactics/nCicElim.ml
index 24fd7d8e9..0840b16a6 100644
--- a/matitaB/components/ng_tactics/nCicElim.ml
+++ b/matitaB/components/ng_tactics/nCicElim.ml
@@ -20,7 +20,7 @@ let fresh_name =
 
 let mk_id id =
  let id = if id = "_" then fresh_name () else id in
-  NotationPt.Ident (id,None)
+  NotationPt.Ident (id,`Ambiguous)
 ;;
 
 (*CSC: cut&paste from nCicReduction.split_prods, but does not check that
@@ -225,9 +225,10 @@ let pp (status: #NCic.status) =
  let rec pp rels =
   function
     NCic.Rel i -> List.nth rels (i - 1)
-  | NCic.Const _ as t ->
+  | NCic.Const r as t ->
      NotationPt.Ident
-      (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,None)
+      (status#ppterm ~metasenv:[] ~subst:[] ~context:[] t,
+       `Uri (NReference.string_of_reference r))
   | NCic.Sort s -> NotationPt.Sort (fst (ast_of_sort s))
   | NCic.Meta _
   | NCic.Implicit _ -> assert false
@@ -280,7 +281,7 @@ let mk_projection status leftno tyname consname consty (projname,_,_) i =
      let arg = mk_id "xxx" in
      let arg_ty = mk_appl (mk_id tyname :: List.rev names) in
      let bvar = mk_id "yyy" in
-     let underscore = NotationPt.Ident ("_",None),None in
+     let underscore = NotationPt.Ident ("_",`Ambiguous),None in
      let bvars =
       HExtlib.mk_list underscore i @ [bvar,None] @
        HExtlib.mk_list underscore (argsno - i -1) in