]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 83def9e) | patch
New command default "foo" uri1 ... urin
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Jul 2005 14:01:46 +0000 (14:01 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Mon, 4 Jul 2005 14:01:46 +0000 (14:01 +0000)
commita9af753c66a80cb4f50f32e63272f3830cba306c
tree10e7fbabbc548be057a1489947eb41423c40e5e3tree | snapshot
parent83def9eb07b5c3c5ddb9e9873677e61b518ec0e2commit | diff
New command   default "foo" uri1 ... urin
to set uri1 ... urin as the default foo.

Actually it can be used to set the current equality, true, false and absurd
like this:

default "equality" equri sym_equri transeq_uri eq_induri eq_ind_ruri.
default "true" trueuri.
default "false" falseuri.
default "absurd" absurduri.
12 files changed:
helm/ocaml/cic/.depend diff | blob | history
helm/ocaml/cic/Makefile diff | blob | history
helm/ocaml/cic/libraryObjects.ml diff | blob | history
helm/ocaml/cic/libraryObjects.mli diff | blob | history
helm/ocaml/cic/matitaLibraryObjects.ml [deleted file] blob | history
helm/ocaml/cic/matitaLibraryObjects.mli [deleted file] blob | history
helm/ocaml/cic_disambiguation/cicTextualParser2.ml diff | blob | history
helm/ocaml/cic_transformations/tacticAst.ml diff | blob | history
helm/ocaml/cic_transformations/tacticAstPp.ml diff | blob | history
helm/ocaml/tactics/discriminationTactics.ml diff | blob | history
helm/ocaml/tactics/equalityTactics.ml diff | blob | history
helm/ocaml/tactics/negationTactics.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.