...

[helm.git] / helm / software / components / grafite_parser / grafiteDisambiguate.ml

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index 8983fdcb91806243117ca6088b512bdab2ba6fa2..ad7f70ef1a331e3430228e74f4e88a71b57e689c 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -46,18 +46,19 @@ let singleton msg = function
       HLog.debug debug; assert false
 
   (** @param term not meaningful when context is given *)
-let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv term =
+let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv
+term =
   let lexicon_status = !lexicon_status_ref in
-  let (diff, metasenv, cic, _) =
+  let (diff, metasenv, subst, cic, _) =
     singleton "first"
       (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
         ~aliases:lexicon_status.LexiconEngine.aliases
         ?goal ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-        ~context ~metasenv (text,prefix_len,term))
+        ~context ~metasenv ~subst:[] (text,prefix_len,term))
   in
   let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
   lexicon_status_ref := lexicon_status;
-  metasenv,cic
+  metasenv,(*subst,*) cic
 ;;
 
   (** disambiguate_lazy_term (circa): term -> (unit -> status) * lazy_term
@@ -68,12 +69,12 @@ let disambiguate_term goal text prefix_len lexicon_status_ref context metasenv t
 let disambiguate_lazy_term goal text prefix_len lexicon_status_ref term =
   (fun context metasenv ugraph ->
     let lexicon_status = !lexicon_status_ref in
-    let (diff, metasenv, cic, ugraph) =
+    let (diff, metasenv, _, cic, ugraph) =
       singleton "second"
         (GrafiteDisambiguator.disambiguate_term ~dbd:(LibraryDb.instance ())
           ~initial_ugraph:ugraph ~aliases:lexicon_status.LexiconEngine.aliases
           ~universe:(Some lexicon_status.LexiconEngine.multi_aliases)
-          ~context ~metasenv ?goal
+          ~context ~metasenv ~subst:[] ?goal
           (text,prefix_len,term)) in
     let lexicon_status = LexiconEngine.set_proof_aliases lexicon_status diff in
     lexicon_status_ref := lexicon_status;
@@ -455,7 +456,7 @@ let disambiguate_obj lexicon_status ?baseuri metasenv (text,prefix_len,obj) =
          | None -> raise BaseUriNotSetYet)
     | CicNotationPt.Inductive _ -> assert false
     | CicNotationPt.Theorem _ -> None in
-  let (diff, metasenv, cic, _) =
+  let (diff, metasenv, _, cic, _) =
     singleton "third"
       (GrafiteDisambiguator.disambiguate_obj ~dbd:(LibraryDb.instance ())
         ~aliases:lexicon_status.LexiconEngine.aliases