X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fcic_disambiguation%2FcicDisambiguate.ml;h=853c38e4b762cb6114c8ccf77db8cddda098e0ef;hb=641ab7e5aa7dbfa352028d7bba95def7234cc3f1;hp=749f1434d2f82a34337fdd9d245d2e377672a084;hpb=11b2157bacf59cfc561c2ef6f92ee41ee2c1a006;p=helm.git diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml index 749f1434d..853c38e4b 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 -> @@ -394,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 -> @@ -480,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 @@ -537,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 @@ -579,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 @@ -613,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