From d4a074601a61f35ab146a1b97014768683e7ee65 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Wed, 26 Dec 2018 19:18:24 +0100 Subject: [PATCH] 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. --- matita/components/ng_disambiguation/grafiteDisambiguate.ml | 6 +++--- matita/components/ng_disambiguation/grafiteDisambiguate.mli | 2 +- 2 files changed, 4 insertions(+), 4 deletions(-) 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: -- 2.39.2