work in progress with voids and lveq (was: the most recent voids)

[helm.git] / helm / software / components / cic_disambiguation / cicDisambiguate.ml

diff --git a/helm/software/components/cic_disambiguation/cicDisambiguate.ml b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
index cf59ab553c33efc202208ea7d0cea86f7734aa74..8f8bba7d81e2ba69923ca1e92cab72109c988296 100644 (file)
--- 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
@@ -645,13 +649,14 @@ let string_context_of_context =
 
 let disambiguate_term ~context ~metasenv ~subst ~expty 
   ?(initial_ugraph = CicUniv.oblivion_ugraph)
-  ~mk_implicit ~description_of_alias ~mk_choice
+  ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
   ~aliases ~universe ~lookup_in_library (text,prefix_len,term)
 =
   let mk_localization_tbl x = Cic.CicHash.create x in
    MultiPassDisambiguator.disambiguate_thing ~context ~metasenv ~subst
     ~initial_ugraph ~aliases ~string_context_of_context
     ~universe ~lookup_in_library ~mk_implicit ~description_of_alias
+    ~fix_instance
     ~uri:None ~pp_thing:CicNotationPp.pp_term
     ~domain_of_thing:Disambiguate.domain_of_term
     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
@@ -661,7 +666,7 @@ let disambiguate_term ~context ~metasenv ~subst ~expty
     ~freshen_thing:CicNotationUtil.freshen_term
     ~passes:(MultiPassDisambiguator.passes ())
 
-let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
+let disambiguate_obj ~mk_implicit ~description_of_alias ~fix_instance ~mk_choice
  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
 =
   let mk_localization_tbl x = Cic.CicHash.create x in
@@ -669,7 +674,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
     ~aliases ~universe ~uri ~string_context_of_context
     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
     ~domain_of_thing:Disambiguate.domain_of_obj
-    ~lookup_in_library ~mk_implicit ~description_of_alias
+    ~lookup_in_library ~mk_implicit ~description_of_alias ~fix_instance
     ~initial_ugraph:CicUniv.empty_ugraph
     ~interpretate_thing:(interpretate_obj ~mk_choice)
     ~refine_thing:refine_obj