]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 134d827) | patch
1) unification hint now takes NG terms (as it should have been from the very
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 23:00:56 +0000 (23:00 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Tue, 16 Jun 2009 23:00:56 +0000 (23:00 +0000)
commitc7a74f0ef29118fc97c1a6283f4249a0ed4b0ba1
treed5b2bac5da9cd623d195418d8dd83de2b7f9cb12tree | snapshot
parent134d8273511016e9b6de3423d301a080046f3948commit | diff
1) unification hint now takes NG terms (as it should have been from the very
   beginning)
2) refresh_uris_in_term is now passed to the constructor of the
   existential/universal data type in NCicLibrary
3) URIs are now refreshed in unification hint data
helm/software/components/grafite/grafiteAst.ml diff | blob | history
helm/software/components/grafite/grafiteAstPp.ml diff | blob | history
helm/software/components/grafite_engine/grafiteEngine.ml diff | blob | history
helm/software/components/grafite_parser/grafiteDisambiguate.ml diff | blob | history
helm/software/components/ng_kernel/nCicLibrary.ml diff | blob | history
helm/software/components/ng_kernel/nCicLibrary.mli diff | blob | history
helm/software/components/ng_refiner/nCicUnifHint.ml diff | blob | history
helm/software/components/ng_refiner/nCicUnifHint.mli diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.