projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2007-09-08
Enrico Tassi
matita can now safely start a matitac that will put...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Enrico Tassi
Full specification of find. Added notation for If_Then_...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
bump version
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
release
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
* add ocamldoc comments to .mli interface files
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
include also gdome2/ dir in the ocamldoc include path
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
* debian/rules
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
why the heck configure was committed?
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
* debian/control
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
init new dummy entry
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
remove spurious comment
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
upload to unstable
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
remove spurious entry
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
- s/Source-Version/binary:Version/ substvar
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
add stdlib/gdome2 to the include dir for ocamldoc
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
bump version
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
* convert comments in .mli interface files to ocamldoc...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-08
Stefano Zacchiroli
convert comments to ocamldoc comments
commit
|
commitdiff
|
tree
|
snapshot
2007-09-07
Enrico Tassi
1. fix_arity fixed: the code is totally wrong and this...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-07
Enrico Tassi
This cast now works!
commit
|
commitdiff
|
tree
|
snapshot
2007-09-07
Enrico Tassi
when a coercion is passed through a case on right-param...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-07
Cristian Armentano
some simplifications.
commit
|
commitdiff
|
tree
|
snapshot
2007-09-07
Enrico Tassi
ooops, missing )
commit
|
commitdiff
|
tree
|
snapshot
2007-09-07
Enrico Tassi
disabled coercions when refining paramod proofs (attemt...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-07
Enrico Tassi
fixed propagation under Fix/Lambda/Case of coercions...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-06
Cristian Armentano
Some simplifications.
commit
|
commitdiff
|
tree
|
snapshot
2007-09-06
Enrico Tassi
coercions under Fix and Case. Code refactoring needed
commit
|
commitdiff
|
tree
|
snapshot
2007-09-06
Enrico Tassi
added a duplicated implementation of replace lifting
commit
|
commitdiff
|
tree
|
snapshot
2007-09-06
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-05
Ferruccio Guidi
- lybrarySync:
commit
|
commitdiff
|
tree
|
snapshot
2007-09-05
Ferruccio Guidi
- matitaInit matitaprover matitadep matitamake:
commit
|
commitdiff
|
tree
|
snapshot
2007-09-05
Claudio Sacerdoti...
added fix case
commit
|
commitdiff
|
tree
|
snapshot
2007-09-05
Claudio Sacerdoti...
coercions are propagated under Fix (but not mutually...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-04
Claudio Sacerdoti...
Dandling ")" removed from notation for 'exists.
commit
|
commitdiff
|
tree
|
snapshot
2007-09-04
Claudio Sacerdoti...
Composition of coercions with arity > 0 is now implemen...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-04
Claudio Sacerdoti...
A test for propagation of coercions (that open new...
commit
|
commitdiff
|
tree
|
snapshot
2007-09-04
Claudio Sacerdoti...
1. composition of coercions with saturations > 0 is...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-31
Claudio Sacerdoti...
alpha conversion to avoid case-insensitivity of MySql...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-31
Claudio Sacerdoti...
baseuri changed
commit
|
commitdiff
|
tree
|
snapshot
2007-08-31
Enrico Tassi
fixed coercions between arrows when the arrow is dependent.
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
captured exception preserved (was replaced blindly...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
reverted assertion, since it may happen to look for...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
refactoring of all coercions code and add a check to...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
bugfix in computation of src and tgt for coercions...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
tests for coercions under lambdas
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Claudio Sacerdoti...
Coercions are now generalized to the general form
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
Coercions rework:
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
coercions from funclass are not supported
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
bla bla bla fallback
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
added a binch of svn:ignore
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
add a fallback in case the binaries are in the path...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
print few more wired assertions
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
the version on the livecd
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
more stuff to reach an intensional definition of finite...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
added an utility function
commit
|
commitdiff
|
tree
|
snapshot
2007-08-30
Enrico Tassi
0.2.0
commit
|
commitdiff
|
tree
|
snapshot
2007-08-28
Claudio Sacerdoti...
* definition of implication free propositional formulas
commit
|
commitdiff
|
tree
|
snapshot
2007-08-28
Claudio Sacerdoti...
A primer for Matita with some easy, medium, difficult...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-26
Ferruccio Guidi
We define proof tree tracks and normal proof tree track...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-26
Ferruccio Guidi
refactoring
commit
|
commitdiff
|
tree
|
snapshot
2007-08-26
Ferruccio Guidi
proof by "introduction" (impi) implemented in full
commit
|
commitdiff
|
tree
|
snapshot
2007-08-25
Claudio Sacerdoti...
thread-based interface activated again
commit
|
commitdiff
|
tree
|
snapshot
2007-08-23
Claudio Sacerdoti...
Bug fixed: RewriteLR were not recognized correctly...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-23
Claudio Sacerdoti...
Bug fixed: the initial metasenv used in the two tactic...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-22
Claudio Sacerdoti...
Avoid reusing Hbeta several times.
commit
|
commitdiff
|
tree
|
snapshot
2007-08-22
Claudio Sacerdoti...
select now works correctly even if multiple hypotheses...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-21
Claudio Sacerdoti...
Avoid confusion for names of proofs put in the applicat...
commit
|
commitdiff
|
tree
|
snapshot
2007-08-21
Claudio Sacerdoti...
"obtain H E1=E2 by proof" is now working
commit
|
commitdiff
|
tree
|
snapshot
2007-08-16
Cristian Armentano
little change to theorem eq_gcd_times_times_eqv_times_gcd
commit
|
commitdiff
|
tree
|
snapshot
2007-07-31
Andrea Asperti
removed generic_sigma_p since generic_iter_p is the...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-31
Enrico Tassi
something was really too slow...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-31
Enrico Tassi
default equality stuff filtered out from hint rewrite
commit
|
commitdiff
|
tree
|
snapshot
2007-07-31
Enrico Tassi
removed comments in proof presentation
commit
|
commitdiff
|
tree
|
snapshot
2007-07-30
Cristian Armentano
renamed generic_sigma_p.ma to generic_iter_p.ma
commit
|
commitdiff
|
tree
|
snapshot
2007-07-30
Enrico Tassi
added 'rewrite' option to the the hint macro. a cicBrow...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-26
Ferruccio Guidi
We add a binary for computing the "heights" of helm...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-26
Enrico Tassi
added development path normalization, inclusions with...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-26
Enrico Tassi
auto -> autobatch
commit
|
commitdiff
|
tree
|
snapshot
2007-07-26
Wilmer Ricciotti
Some notation added
commit
|
commitdiff
|
tree
|
snapshot
2007-07-26
Enrico Tassi
more stuff about coercions
commit
|
commitdiff
|
tree
|
snapshot
2007-07-26
Enrico Tassi
little bug in coercion generation found. it use to...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-26
Ferruccio Guidi
makefiles updated
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Ferruccio Guidi
makefile updated
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Ferruccio Guidi
matitac: We do not generate the .moo and .lexicon of...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Enrico Tassi
added some notation
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Enrico Tassi
added another example in which our coercions are powerful
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Enrico Tassi
used ;try assumption instead of .try assumption
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Enrico Tassi
; and not . after auto-paramodulation
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Enrico Tassi
reverted previous fix
commit
|
commitdiff
|
tree
|
snapshot
2007-07-25
Enrico Tassi
restored compaction of metas at the end of given_clause
commit
|
commitdiff
|
tree
|
snapshot
2007-07-24
Ferruccio Guidi
Makefile missing in previous commit
commit
|
commitdiff
|
tree
|
snapshot
2007-07-24
Ferruccio Guidi
New developement LOGIC about the cut elimination of...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-24
Enrico Tassi
added test about dependent coercions
commit
|
commitdiff
|
tree
|
snapshot
2007-07-23
Claudio Sacerdoti...
Prototype of min_aux changed.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-23
Ferruccio Guidi
auto vs autobatch fixed
commit
|
commitdiff
|
tree
|
snapshot
2007-07-23
Ferruccio Guidi
autobatch parameters reajusted
commit
|
commitdiff
|
tree
|
snapshot
2007-07-23
Enrico Tassi
fixed makefiles to make it compile cleanly again
commit
|
commitdiff
|
tree
|
snapshot
2007-07-22
Ferruccio Guidi
Procedural: the statement body and it inner types must...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-20
Claudio Sacerdoti...
Another nicer version.
commit
|
commitdiff
|
tree
|
snapshot
next