X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=7ebca20d763f41043577fd1ed953f38fd987c10e;hb=ca854dac6ac2fac7a9ab78b6cc3bc98e3d3e20cc;hp=d50eec79600b12358ecd7bc5af9d84f4ae7f4d47;hpb=7288b45eacf9f7dcd118b3b89b81ff19ae9d6ce5;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index d50eec796..7ebca20d7 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -332,6 +332,10 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
+    | CicNotationPt.NCic t -> 
+           let context = (* to make metas_of_term happy *)
+             List.map (fun x -> x,NCic.Decl (NCic.Implicit `Type)) context in
+           assert(NCicUntrusted.metas_of_term [] context t = []); t
     | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | CicNotationPt.Implicit (`Tagged s) -> NCic.Implicit (`Tagged s)
@@ -610,7 +614,7 @@ let interpretate_obj
 ;;
 
 let disambiguate_term ~context ~metasenv ~subst ~expty
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library 
    (text,prefix_len,term) 
  =
@@ -619,7 +623,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_term
      ~context ~metasenv ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe ~uri:None ~pp_thing:CicNotationPp.pp_term
      ~passes:(MultiPassDisambiguator.passes ())
@@ -632,7 +636,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
 ;;
 
 let disambiguate_obj 
-   ~mk_implicit ~description_of_alias ~mk_choice
+   ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
    ~aliases ~universe ~rdb ~lookup_in_library ~uri
    (text,prefix_len,obj) 
  =
@@ -641,7 +645,7 @@ let disambiguate_obj
     MultiPassDisambiguator.disambiguate_thing
      ~freshen_thing:CicNotationUtil.freshen_obj
      ~context:[] ~metasenv:[] ~subst:[] ~initial_ugraph:() ~aliases
-     ~mk_implicit ~description_of_alias
+     ~mk_implicit ~description_of_alias ~fix_instance
      ~string_context_of_context:(List.map (fun (x,_) -> Some x))
      ~universe 
      ~uri:(Some uri)