]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9efaf66) | 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)
commit08a92d276c5477968b02f31097b6ed03185f34eb
treee242c98016f88d66279f104b8f7415afa1eed7f4tree | snapshot
parent9efaf66294d18446b7cd960f9ed4203799073e62commit | 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:
helm/software/components/cic/libraryObjects.ml diff | blob | history
helm/software/components/cic/libraryObjects.mli diff | blob | history
helm/software/components/library/librarySync.ml diff | blob | history
helm/software/components/tactics/discriminationTactics.ml diff | blob | history
helm/software/components/tactics/equalityTactics.ml diff | blob | history
helm/software/components/tactics/inversion.ml diff | blob | history
helm/software/components/tactics/inversion.mli diff | blob | history
helm/software/components/tactics/inversion_principle.ml diff | blob | history
helm/software/components/tactics/metadataQuery.ml diff | blob | history
helm/software/components/tactics/negationTactics.ml diff | blob | history
helm/software/components/tactics/paramodulation/equality.ml diff | blob | history
helm/software/components/tactics/paramodulation/indexing.ml diff | blob | history
helm/software/components/tactics/paramodulation/inference.ml diff | blob | history
helm/software/components/tactics/paramodulation/saturation.ml diff | blob | history
helm/software/components/tactics/paramodulation/utils.ml diff | blob | history
helm/software/components/tactics/paramodulation/utils.mli diff | blob | history
helm/software/matita/library/legacy/coq.ma diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.