]> matita.cs.unibo.it Git - helm.git/commit
Huge commit:
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Dec 2006 13:41:38 +0000 (13:41 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 14 Dec 2006 13:41:38 +0000 (13:41 +0000)
commit5d010a40c726d9a7eceeb35e70e41a158eb63c70
tree5ba2ecd29b87314df32cbfeb327574fe211e2088
parent55444711ececb62f0a93f2a064f64c3b27f744e2
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).
23 files changed:
helm/software/components/acic_content/acic2content.ml
helm/software/components/acic_content/termAcicContent.ml
helm/software/components/cic_unification/.depend
helm/software/components/cic_unification/Makefile
helm/software/components/cic_unification/cicRefine.ml
helm/software/components/cic_unification/cicUnification.ml
helm/software/components/cic_unification/coercGraph.ml [new file with mode: 0644]
helm/software/components/cic_unification/coercGraph.mli [new file with mode: 0644]
helm/software/components/cic_unification/termUtil.ml [new file with mode: 0644]
helm/software/components/cic_unification/termUtil.mli [new file with mode: 0644]
helm/software/components/library/.depend
helm/software/components/library/Makefile
helm/software/components/library/coercDb.ml
helm/software/components/library/coercDb.mli
helm/software/components/library/coercGraph.ml [deleted file]
helm/software/components/library/coercGraph.mli [deleted file]
helm/software/components/library/librarySync.ml
helm/software/components/tactics/auto.ml
helm/software/components/tactics/equalityTactics.ml
helm/software/components/tactics/primitiveTactics.ml
helm/software/components/tactics/proofEngineHelpers.ml
helm/software/components/tactics/proofEngineHelpers.mli
helm/software/components/tactics/universe.ml