]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: d1161f5) | patch
1. the default for the default equality/absurd/true/false URIs used to be
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Jun 2006 14:39:14 +0000 (14:39 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Fri, 9 Jun 2006 14:39:14 +0000 (14:39 +0000)
commitec7717f5e0dd4c295ba1cfd57a0a6a46170490ef
tree0463f120ccc5f8038dd39ba6fc97ad7268187173tree | snapshot
parentd1161f58d1537528aa2810706819f5251a0954d9commit | diff
1. the default for the default equality/absurd/true/false URIs used to be
   the Coq ones; now it is None
2. legacy/coq.ma changed to set the default URIs for Coq
3. generation of inversion principles is now branched again
17 files changed:
components/cic/libraryObjects.ml diff | blob | history
components/cic/libraryObjects.mli diff | blob | history
components/library/librarySync.ml diff | blob | history
components/tactics/discriminationTactics.ml diff | blob | history
components/tactics/equalityTactics.ml diff | blob | history
components/tactics/inversion.ml diff | blob | history
components/tactics/inversion.mli diff | blob | history
components/tactics/inversion_principle.ml diff | blob | history
components/tactics/metadataQuery.ml diff | blob | history
components/tactics/negationTactics.ml diff | blob | history
components/tactics/paramodulation/equality.ml diff | blob | history
components/tactics/paramodulation/indexing.ml diff | blob | history
components/tactics/paramodulation/inference.ml diff | blob | history
components/tactics/paramodulation/saturation.ml diff | blob | history
components/tactics/paramodulation/utils.ml diff | blob | history
components/tactics/paramodulation/utils.mli diff | blob | history
matita/library/legacy/coq.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.