X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=db305e5d5be35be6263eadca1fba077b1db66418;hb=d5f1d21626a9df44030854abe3b96bb71c6348af;hp=3e9124e69bd2398c3eef1a02241d4154d1c607b7;hpb=b225178112c2c5ef1a717ac7e647d854d94b2e52;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index 3e9124e69..db305e5d5 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -352,9 +352,13 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
               in
               let cic_body =
                aux ~localize loc context' (add_binders `Lambda body) in
+              let typ =
+               match typ with
+                  Some typ -> typ
+                | None-> CicNotationPt.Implicit `JustOne in
               let cic_type =
                aux_option ~localize loc context (Some `Type)
-                (HExtlib.map_option (add_binders `Pi) typ) in
+                (Some (add_binders `Pi typ)) in
               let name =
                 match CicNotationUtil.cic_name_of_name name with
                 | Cic.Anonymous ->
@@ -392,8 +396,10 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
                 List.fold_right (build_term inductiveFuns) inductiveFuns
                  cic_body)
     | CicNotationPt.Ident _
-    | CicNotationPt.Uri _ when is_path -> raise Disambiguate.PathNotWellFormed
-    | CicNotationPt.Ident (name, subst)
+    | CicNotationPt.Uri _
+    | CicNotationPt.NRef _ when is_path -> raise Disambiguate.PathNotWellFormed
+    | CicNotationPt.NRef _ -> assert false
+    | CicNotationPt.Ident (name,subst)
     | CicNotationPt.Uri (name, subst) as ast ->
         let is_uri = function CicNotationPt.Uri _ -> true | _ -> false in
         (try
@@ -478,7 +484,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
@@ -496,6 +503,7 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | CicNotationPt.Sort `Set -> Cic.Sort Cic.Set
     | CicNotationPt.Sort (`Type u) -> Cic.Sort (Cic.Type u)
     | CicNotationPt.Sort (`NType _) -> Cic.Sort (Cic.Type (CicUniv.fresh ()))
+    | CicNotationPt.Sort (`NCProp _) -> Cic.Sort (Cic.CProp (CicUniv.fresh ()))
     | CicNotationPt.Sort (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~mk_choice ~env
@@ -534,7 +542,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
@@ -576,7 +584,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