From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Wed, 26 Dec 2018 18:18:24 +0000 (+0100)
Subject: Matita 0.99.* bug fixed: new alias insertion
X-Git-Tag: make_still_working~229^2~1^2~18
X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=commitdiff_plain;h=062205f9595812819a8783df5b578a5683b27d09

Matita 0.99.* bug fixed: new alias insertion

Fixed a bug that was there since the new Matita
generation: new_aliases were always computed
as empty and thus never inserted.
---

diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.ml b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
index 9cfbbc8c0..7b1e2c508 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.ml
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.ml
@@ -57,9 +57,9 @@ class virtual status =
 let eval_with_new_aliases status f =
  let status =
   status#set_disambiguate_db { status#disambiguate_db with new_aliases = [] } in
- let res = f status in
- let new_aliases = status#disambiguate_db.new_aliases in
-  new_aliases,res
+ let new_status = f status in
+ let new_aliases = new_status#disambiguate_db.new_aliases in
+  new_aliases,new_status
 ;;
 
 let dump_aliases out msg status =
diff --git a/matita/components/ng_disambiguation/grafiteDisambiguate.mli b/matita/components/ng_disambiguation/grafiteDisambiguate.mli
index c462af36f..019051255 100644
--- a/matita/components/ng_disambiguation/grafiteDisambiguate.mli
+++ b/matita/components/ng_disambiguation/grafiteDisambiguate.mli
@@ -40,7 +40,7 @@ class virtual status :
  end
 
 val eval_with_new_aliases:
- #status as 'status -> ('status -> 'a) ->
+ #status as 'status -> ('status -> (#status as 'a)) ->
   (DisambiguateTypes.domain_item * GrafiteAst.alias_spec) list * 'a
 
 val set_proof_aliases: