]> matita.cs.unibo.it Git - helm.git/commit
projects / helm.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 04fcadb) | patch
1 .Tactic generalize ported to patterns and activated in matita.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 23 Jun 2005 12:14:53 +0000 (12:14 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Thu, 23 Jun 2005 12:14:53 +0000 (12:14 +0000)
commit6a9b5c500ba77d823730202fb9b0c5fcb5b269de
tree4dee5741ed55287bb3e0eb91a4680d91f5b4697ftree | snapshot
parent04fcadbd9e194847138d97a0a9892a475bc21c88commit | diff
1 .Tactic generalize ported to patterns and activated in matita.
2. new syntax for patterns:
   "in H0 [: ty] ; ... ; Hn [: ty] [\vdash ty]"
   where the list of hypotheses may be empty
helm/ocaml/cic_disambiguation/cicTextualParser2.ml diff | blob | history
Unnamed repository; edit this file 'description' to name the repository.