From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 14 Dec 2006 13:41:38 +0000 (+0000)
Subject: Huge commit:
X-Git-Tag: 0.4.95@7852~735
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=6bb370c6e1a036e82315765d6dceb1939c30ed23;hp=6bb370c6e1a036e82315765d6dceb1939c30ed23;p=helm.git

Huge commit:

 1. coercGraph.ml* moved from library to cic_unification (where it should
    have been put in the first place). A few functions that must remain in
   library moved to coercDb.ml* (where they should have been put in the first
   place)
 2. ProofEngineHelpers.saturate_term moved from tactic to cic_unification.
 3. Bug fixed in saturate_term: the newmeta returned by the function was not
    correct in some cases
 4. CoercGraph.look_for_coercion* used to saturate the coercion with implicit
    arguments (thus requirin a refinement pass later on). Now the same
    functions saturate the term with metas. The return type has changed
    accordingly.
 5. the horrible hack to break composite coercions during unification has been
    replaced by a nice implementation of unification towards the join of the
    two coercions (called meet by Enrico I do not know why :-).
    This solves many many problems found using multiple coercion pathes from
    a source to a destination. (This is the case in DAMA that I am going to
    commit soon).
---