X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=853c38e4b762cb6114c8ccf77db8cddda098e0ef;hb=34c2ba63c8eb5fccfd9a1fb8ac1df5895c8b58b3;hp=cf59ab553c33efc202208ea7d0cea86f7734aa74;hpb=0e1bf8990c7c3100f5c5ca50c99ead4f3858e76f;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index cf59ab553..853c38e4b 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -353,7 +353,9 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
               let cic_body =
                aux ~localize loc context' (add_binders `Lambda body) in
               let typ =
-               match typ with Some typ -> typ | None-> CicNotationPt.Implicit in
+               match typ with
+                  Some typ -> typ
+                | None-> CicNotationPt.Implicit `JustOne in
               let cic_type =
                aux_option ~localize loc context (Some `Type)
                 (Some (add_binders `Pi typ)) in
@@ -396,6 +398,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | CicNotationPt.Ident _
     | CicNotationPt.Uri _
     | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.NCic _ -> assert false
     | CicNotationPt.NRef _ -> assert false
     | CicNotationPt.Ident (name,subst)
     | CicNotationPt.Uri (name, subst) as ast ->
@@ -482,7 +485,8 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
            with 
              CicEnvironment.CircularDependency _ -> 
                raise (DisambiguateTypes.Invalid_choice (lazy (loc,"Circular dependency in the environment")))))
-    | CicNotationPt.Implicit -> Cic.Implicit None
+    | CicNotationPt.Implicit `Vector -> assert false
+    | CicNotationPt.Implicit (`JustOne | `Tagged _) -> Cic.Implicit None
     | CicNotationPt.UserInput -> Cic.Implicit (Some `Hole)
     | CicNotationPt.Num (num, i) ->
        Disambiguate.resolve ~mk_choice ~env
@@ -539,7 +543,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
         (fun (context,res) (name,t) ->
           let t =
            match t with
-              None -> CicNotationPt.Implicit
+              None -> CicNotationPt.Implicit `JustOne
             | Some t -> t in
           let name = CicNotationUtil.cic_name_of_name name in
            name::context,(name, interpretate_term context env None false t)::res
@@ -581,7 +585,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
         (fun (context,res) (name,t) ->
           let t =
            match t with
-              None -> CicNotationPt.Implicit
+              None -> CicNotationPt.Implicit `JustOne
             | Some t -> t in
           let name = CicNotationUtil.cic_name_of_name name in
            name::context,(name, interpretate_term context env None false t)::res
@@ -615,7 +619,7 @@ let interpretate_obj ~mk_choice ~context ~env ~uri ~is_path obj
      let field_names = List.map (fun (x,_,y,z) -> x,y,z) fields in
       Cic.InductiveDefinition
        (tyl,[],List.length params,[`Class (`Record field_names)])
-  | CicNotationPt.Theorem (flavour, name, ty, bo) ->
+  | CicNotationPt.Theorem (flavour, name, ty, bo, _pragma) ->
      let attrs = [`Flavour flavour] in
      let ty' = interpretate_term [] env None false ty in
      (match bo,flavour with