Stricter type: the type now shows that disambiguation only alter the lexicon.

In this way we are forced to manually set the content of the object in place of
setting the whole object, that leads to information loss since in the meanwhile
new commands may have altered the rest of the state.

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.ml b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
index a0558d9f65a06af2f3703d3826f5f4a678339092..6b5dfca61b829235b852cdc4e7f0a44cd6d52501 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.ml
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.ml
@@ -633,6 +633,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
    in
      UriManager.uri_of_string (baseuri ^ "/" ^ name)
   in
+(*
  let _try_new cic =
   (NCicLibrary.clear_cache ();
    NCicEnvironment.invalidate ();
@@ -721,6 +722,7 @@ let disambiguate_obj estatus ?baseuri metasenv (text,prefix_len,obj) =
        )
   )
  in 
+*)
 
 
  try

diff --git a/helm/software/components/grafite_parser/grafiteDisambiguate.mli b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
index 0592de671e9fe18cd2c75398248ce12588c5cae5..6565a4d9f0e4887091929e8fec214662597d6a1f 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteDisambiguate.mli
+++ b/helm/software/components/grafite_parser/grafiteDisambiguate.mli
@@ -35,21 +35,21 @@ type lazy_tactic =
     GrafiteAst.tactic
 
 val disambiguate_tactic:
- #LexiconEngine.status ref ->
+ LexiconEngine.status ref ->
  Cic.context ->
  Cic.metasenv -> int option ->
  tactic Disambiguate.disambiguator_input ->
   Cic.metasenv * lazy_tactic
 
 val disambiguate_command: 
- #NEstatus.status as 'status ->
+ LexiconEngine.status as 'status ->
  ?baseuri:string ->
  Cic.metasenv ->
  ((CicNotationPt.term,CicNotationPt.term CicNotationPt.obj) GrafiteAst.command) Disambiguate.disambiguator_input ->
   'status * Cic.metasenv * (Cic.term,Cic.obj) GrafiteAst.command
 
 val disambiguate_macro:
- #LexiconEngine.status ref ->
+ LexiconEngine.status ref ->
  Cic.metasenv ->
  Cic.context ->
  ((CicNotationPt.term,CicNotationPt.term) GrafiteAst.macro) Disambiguate.disambiguator_input ->

diff --git a/helm/software/matita/matitaEngine.ml b/helm/software/matita/matitaEngine.ml
index 6e6213734d583422c5732471376ea3e0ff640869..6b16891c883621460ccfb5c7133eebd4aa465067 100644 (file)
--- a/helm/software/matita/matitaEngine.ml
+++ b/helm/software/matita/matitaEngine.ml
@@ -61,7 +61,7 @@ let disambiguate_macro lexicon_status_ref grafite_status macro context =
 let eval_ast ?do_heavy_checks grafite_status (text,prefix_len,ast) =
  let lexicon_status = GrafiteTypes.get_estatus grafite_status in
  let dump = not (Helm_registry.get_bool "matita.moo") in
- let lexicon_status_ref = ref lexicon_status in
+ let lexicon_status_ref = ref (lexicon_status :> LexiconEngine.status) in
  let baseuri = GrafiteTypes.get_baseuri grafite_status in
  let new_grafite_status,new_objs =
   match ast with