projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
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
2007-07-20
Claudio Sacerdoti...
Even nicer script.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-20
Claudio Sacerdoti...
The nicest script obtained so far.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-20
Ferruccio Guidi
acic_procedural: bug fix:
commit
|
commitdiff
|
tree
|
snapshot
2007-07-20
Claudio Sacerdoti...
More simplification due to the new conversion strategy.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-20
Claudio Sacerdoti...
Script simplification due to the new efficient conversi...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-20
Claudio Sacerdoti...
Tentative bug fix for diverging pretty-printing function.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-20
Claudio Sacerdoti...
Initialization of matita.map_unicode_to_tex moved from...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Ferruccio Guidi
cicUtil : new test function "is_sober" to test...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Claudio Sacerdoti...
Convertibility now converts machines in place of terms.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Claudio Sacerdoti...
map_unicode_to_tex is no longer optional and it always...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Claudio Sacerdoti...
paste_unicode_as_tex is now false by default; moreover...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Enrico Tassi
COERCIONS: tentative addition of an equivalence relatio...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Enrico Tassi
the cade was escaping the table name and not the uri
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Enrico Tassi
fixed escaping for sqlite
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Enrico Tassi
fixed an escaping error, added more infos to the generi...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Claudio Sacerdoti...
Typo fixed.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-19
Claudio Sacerdoti...
Super-nice notation for the assembly stuff.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-18
Ferruccio Guidi
the predicate for elim was not built correctly when...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-18
Enrico Tassi
recursive argument in let rec is not printed explicitly.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-18
Enrico Tassi
fixed coercion graph print, moved coercion graph and...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-17
Claudio Sacerdoti...
added missing parenthesis
commit
|
commitdiff
|
tree
|
snapshot
2007-07-17
Enrico Tassi
fixed includes and added notation for bytes
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
More lemmas.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
More daemons closed. A couple left in byte and many...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
More daemons/axioms closed.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
One daemon less.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
More daemons got rid of (and more extra axioms to be...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
Last daemon killed :-)
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
One less daemon (about "update"s).
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
All sub-proofs about "update" closed.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Claudio Sacerdoti...
assembly.ma splitted into many files
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
* NOT RELEASED YET
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
* NOT RELEASED YET
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
proper path for ps.gz doc
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
texlive-base-bin, texlive-latex-extra
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
- add build-dep for doc generation: graphviz, texlive...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
- add build-dep for doc generation: graphviz, texlive...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
* debian/rules
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
invoke make doc after build to create ocamldoc docs
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
* debian/svn-deblayout
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
* rebuild against OCaml 3.10 and ocamlnet 2.2
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
* debian/*.install.in
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Stefano Zacchiroli
* rebuild with OCaml 3.10
commit
|
commitdiff
|
tree
|
snapshot
2007-07-16
Wilmer Ricciotti
corrected axiom mod_plus
commit
|
commitdiff
|
tree
|
snapshot
2007-07-14
Ferruccio Guidi
new definitions and new theorems
commit
|
commitdiff
|
tree
|
snapshot
2007-07-13
Claudio Sacerdoti...
More conjectures closed.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-13
Claudio Sacerdoti...
1. requires the new pretty printer for natural numbers
commit
|
commitdiff
|
tree
|
snapshot
2007-07-13
Claudio Sacerdoti...
Dirty patch by Zack: natural numbers of Matita are...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-13
Claudio Sacerdoti...
Last crazy commit reverted.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-13
Claudio Sacerdoti...
Final theorem proved. Many many conjectures left. I...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-12
Claudio Sacerdoti...
The loop invariant I chosed was not correct!
commit
|
commitdiff
|
tree
|
snapshot
2007-07-11
Claudio Sacerdoti...
Getting close to the final result.
commit
|
commitdiff
|
tree
|
snapshot
2007-07-11
Claudio Sacerdoti...
1. loop invariant stated, but not proved
commit
|
commitdiff
|
tree
|
snapshot
2007-07-11
Ferruccio Guidi
native dependences fixed
commit
|
commitdiff
|
tree
|
snapshot
2007-07-11
Claudio Sacerdoti...
1. status factorized out in tick
commit
|
commitdiff
|
tree
|
snapshot
2007-07-11
Claudio Sacerdoti...
auto new => autobatch
commit
|
commitdiff
|
tree
|
snapshot
2007-07-11
Claudio Sacerdoti...
auto new => autobatch
commit
|
commitdiff
|
tree
|
snapshot
2007-07-10
Claudio Sacerdoti...
0. less nice solution by Enrico reverted
commit
|
commitdiff
|
tree
|
snapshot
2007-07-10
Claudio Sacerdoti...
New reduction strategy: the new reduction strategy...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-10
Enrico Tassi
La programmazione funzionale e' come TeX, funziona...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-10
Ferruccio Guidi
persistent inner types are now generated in publishing...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-10
Enrico Tassi
fixed a bug in the cleanup ofsedir that was not properl...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-10
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2007-07-09
Enrico Tassi
1. bug fixed in tick
commit
|
commitdiff
|
tree
|
snapshot
2007-07-09
Enrico Tassi
signal hadler restored after runnig external 'make'
commit
|
commitdiff
|
tree
|
snapshot
2007-07-09
Claudio Sacerdoti...
Interesting theorem added (but still to be proved).
commit
|
commitdiff
|
tree
|
snapshot
2007-07-09
Enrico Tassi
added few more fun to this test
commit
|
commitdiff
|
tree
|
snapshot
2007-07-09
Ferruccio Guidi
new configuration file sample
commit
|
commitdiff
|
tree
|
snapshot
next