From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 18 Jun 2009 09:17:53 +0000 (+0000)
Subject: Stricter type: the type now shows that disambiguation only alter the lexicon.
X-Git-Tag: make_still_working~3853
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=7477c3dbbc2fafe248d48302be0d6ba4cb38d062;p=helm.git

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 a0558d9f6..6b5dfca61 100644
--- 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 0592de671..6565a4d9f 100644
--- 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 6e6213734..6b16891c8 100644
--- 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