New version of deep_subsumption

[helm.git] / matita / matitaEngine.ml

diff --git a/matita/matitaEngine.ml b/matita/matitaEngine.ml
index f0d8ee46c7820b34feff186135edcd418b9b4fd4..18022691cd27c953bf8a9b3a49bfc0611e80d3f5 100644 (file)
--- a/matita/matitaEngine.ml
+++ b/matita/matitaEngine.ml
@@ -93,7 +93,7 @@ let eval_ast ?do_heavy_checks ?clean_baseuri lexicon_status
         LexiconEngine.set_proof_aliases lexicon_status [k,value]
        in
         new_lexicon_status,
-         ((new_grafite_status,new_lexicon_status),Some (k,value))::acc
+         ((grafite_status,new_lexicon_status),Some (k,value))::acc
    ) (lexicon_status,[]) new_aliases
  in
   ((new_grafite_status,new_lexicon_status),None)::intermediate_states