X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_disambiguation%2FnCicDisambiguate.ml;h=357f9e53977aa10be34f8df4b805304d5cd92041;hb=db235934efa41a0f38e79747f6db4f468367410b;hp=108c845c69670eb8b6e5aa44c129d357da1e6ed1;hpb=dcdbb979433a61e2ef2842d96604098728824416;p=helm.git

diff --git a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
index 108c845c6..357f9e539 100644
--- a/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
+++ b/helm/software/components/ng_disambiguation/nCicDisambiguate.ml
@@ -47,9 +47,8 @@ let refine_term
     in
     let metasenv, subst, term, _ = 
       NCicRefiner.typeof 
-        { rdb with NRstatus.coerc_db = 
-           if use_coercions then rdb.NRstatus.coerc_db 
-           else NCicCoercion.empty_db }
+        (rdb#set_coerc_db 
+          (if use_coercions then rdb#coerc_db else NCicCoercion.empty_db))
         metasenv subst context term expty ~localise 
     in
      Disambiguate.Ok (term, metasenv, subst, ())
@@ -79,9 +78,9 @@ let refine_obj
   try
     let obj =
       NCicRefiner.typeof_obj
-        { rdb with NRstatus.coerc_db = 
-           if use_coercions then rdb.NRstatus.coerc_db 
-           else NCicCoercion.empty_db }
+        (rdb#set_coerc_db
+           (if use_coercions then rdb#coerc_db 
+            else NCicCoercion.empty_db))
         obj ~localise 
     in
       Disambiguate.Ok (obj, [], [], ())
@@ -325,7 +324,8 @@ let interpretate_term_and_interpretate_term_option
         with NRef.IllFormedReference _ ->
          CicNotationPt.fail loc "Ill formed reference")
     | CicNotationPt.NRef nref -> NCic.Const nref
-    | CicNotationPt.Implicit -> NCic.Implicit `Term
+    | CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
+    | CicNotationPt.Implicit `JustOne -> NCic.Implicit `Term
     | CicNotationPt.UserInput -> NCic.Implicit `Hole
     | CicNotationPt.Num (num, i) -> 
         Disambiguate.resolve ~env ~mk_choice (Num i) (`Num_arg num)
@@ -363,7 +363,8 @@ let interpretate_term_and_interpretate_term_option
         res
     | Some (CicNotationPt.AttributedTerm (_, term)) ->
         aux_option ~localize loc context annotation (Some term)
-    | Some CicNotationPt.Implicit -> NCic.Implicit annotation
+    | Some CicNotationPt.Implicit `JustOne -> NCic.Implicit annotation
+    | Some CicNotationPt.Implicit `Vector -> NCic.Implicit `Vector
     | Some term -> aux ~localize loc context term
   in
    (fun ~context -> aux ~localize:true HExtlib.dummy_floc context),
@@ -494,7 +495,7 @@ let interpretate_obj
        (fun (context,res) (name,t) ->
          let t =
           match t with
-             None -> CicNotationPt.Implicit
+             None -> CicNotationPt.Implicit `JustOne
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =
@@ -552,7 +553,7 @@ let interpretate_obj
        (fun (context,res) (name,t) ->
          let t =
           match t with
-             None -> CicNotationPt.Implicit
+             None -> CicNotationPt.Implicit `JustOne
            | Some t -> t in
          let name = cic_name_of_name name in
          let t =