....

[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 288be5fa2d5b06fc11a51d4cd682a1b33c1f068c..ed28894a7f6320c0f326c5b3fbf3ce07c911c2e6 100644 (file)
--- a/helm/software/components/cic_disambiguation/cicDisambiguate.ml
+++ b/helm/software/components/cic_disambiguation/cicDisambiguate.ml
@@ -484,11 +484,15 @@ let interpretate_term ~mk_choice ?(create_dummy_ids=false) ~context ~env ~uri
     | CicNotationPt.Sort `Prop -> Cic.Sort Cic.Prop
     | 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 (`CProp u) -> Cic.Sort (Cic.CProp u)
     | CicNotationPt.Symbol (symbol, instance) ->
         Disambiguate.resolve ~mk_choice ~env
          (DisambiguateTypes.Symbol (symbol, instance)) (`Args [])
-    | _ -> assert false (* god bless Bologna *)
+    | CicNotationPt.Variable _
+    | CicNotationPt.Magic _
+    | CicNotationPt.Layout _
+    | CicNotationPt.Literal _ -> assert false (* god bless Bologna *)
   and aux_option ~localize loc context annotation = function
     | None -> Cic.Implicit annotation
     | Some term -> aux ~localize loc context term
@@ -642,7 +646,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
             | _ -> assert false) 
         | k -> k
   in
-  let localization_tbl = Cic.CicHash.create 503 in
+  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
@@ -650,7 +654,7 @@ let disambiguate_term ~context ~metasenv ~subst ?goal
     ~domain_of_thing:Disambiguate.domain_of_term
     ~interpretate_thing:(interpretate_term (?create_dummy_ids:None) ~mk_choice)
     ~refine_thing:refine_term (text,prefix_len,term)
-    ~localization_tbl
+    ~mk_localization_tbl
     ~hint
     ~freshen_thing:CicNotationUtil.freshen_term
     ~passes:(MultiPassDisambiguator.passes ())
@@ -659,7 +663,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
  ~aliases ~universe ~lookup_in_library ~uri (text,prefix_len,obj)
 =
   let hint = (fun _ x -> x), fun k -> k in
-  let localization_tbl = Cic.CicHash.create 503 in
+  let mk_localization_tbl x = Cic.CicHash.create x in
   MultiPassDisambiguator.disambiguate_thing ~context:[] ~metasenv:[] ~subst:[] 
     ~aliases ~universe ~uri ~string_context_of_context
     ~pp_thing:(CicNotationPp.pp_obj CicNotationPp.pp_term)
@@ -668,7 +672,7 @@ let disambiguate_obj ~mk_implicit ~description_of_alias ~mk_choice
     ~initial_ugraph:CicUniv.empty_ugraph
     ~interpretate_thing:(interpretate_obj ~mk_choice)
     ~refine_thing:refine_obj
-    ~localization_tbl
+    ~mk_localization_tbl
     ~hint
     ~passes:(MultiPassDisambiguator.passes ())
     ~freshen_thing:CicNotationUtil.freshen_obj