]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 85d772f) | patch
The Blob is not abstracted on the context any more.
authorAndrea Asperti <andrea.asperti@unibo.it>
Tue, 20 Sep 2011 14:00:34 +0000 (14:00 +0000)
committerAndrea Asperti <andrea.asperti@unibo.it>
Tue, 20 Sep 2011 14:00:34 +0000 (14:00 +0000)
commit97e59118f8cc0d98c51c0d41e8e7704344666cdb
treef4d69199a189c3c35e5275c7511c2e5a7bfc49e4tree | snapshot
parent85d772f5c3d5c86bbb474ba7ab4a259dc06687f9commit | diff
The Blob is not abstracted on the context any more.
The saturate function (that requires the environment now
contained in the status) is now external to the module.
It is defined in NCicBlob.
The functions mk_passive and mk_goals are now expecting
input terms already saturated.
matitaB/components/ng_paramodulation/nCicBlob.ml diff | blob | history
matitaB/components/ng_paramodulation/nCicBlob.mli diff | blob | history
matitaB/components/ng_paramodulation/nCicParamod.ml diff | blob | history
matitaB/components/ng_paramodulation/nCicParamod.mli diff | blob | history
matitaB/components/ng_paramodulation/nCicProof.ml diff | blob | history
matitaB/components/ng_paramodulation/paramod.ml diff | blob | history
matitaB/components/ng_paramodulation/paramod.mli diff | blob | history
matitaB/components/ng_paramodulation/terms.ml diff | blob | history
matitaB/components/ng_paramodulation/terms.mli diff | blob | history
matitaB/components/ng_tactics/nnAuto.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.