X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=cf59ab553c33efc202208ea7d0cea86f7734aa74;hb=7f9e313fe5ae4200f080f481a6b8b795a0618093;hp=b869536bf495cf5e3046a144be2bb39a1d983cde;hpb=df753672ee6c511b6ce721c2124e3294d0a28dbd;p=helm.git

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index b869536bf..cf59ab553 100644
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -352,9 +352,11 @@ 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 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 +394,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