]> matita.cs.unibo.it Git - helm.git/history - matita/tests
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
little bug in coercion generation found. it use to create more coercions that expecte...
[helm.git] / matita / tests /
2007-07-25 Enrico Tassiadded another example in which our coercions are powerful tree | commitdiff
2007-07-25 Enrico Tassiused ;try assumption instead of .try assumption tree | commitdiff
2007-07-24 Enrico Tassiadded test about dependent coercions tree | commitdiff
2007-07-23 Ferruccio Guidiauto vs autobatch fixed tree | commitdiff
2007-07-18 Enrico Tassifixed coercion graph print, moved coercion graph and... tree | commitdiff
2007-07-10 Enrico Tassi... tree | commitdiff
2007-07-09 Enrico Tassiadded few more fun to this test tree | commitdiff
2007-07-09 Enrico Tassiauto->autobatch tree | commitdiff
2007-06-04 Enrico Tassinew more flexible compose, see matita/tests/compose... tree | commitdiff
2007-05-25 Enrico Tassiauto --> autobatch tree | commitdiff
2007-05-25 Enrico Tassiauto --> autobatch tree | commitdiff
2007-05-20 Ferruccio GuidiapplyTransformation: added debugging information tree | commitdiff
2007-04-23 Claudio Sacerdoti... Deprecated "goal" removed. tree | commitdiff
2007-04-20 Claudio Sacerdoti... A new test on some non punctuation tacticals. tree | commitdiff
2007-04-17 Enrico Tassi... tree | commitdiff
2007-04-10 Enrico Tassiset -> type tree | commitdiff
2007-04-10 Enrico Tassi... tree | commitdiff
2007-04-03 Enrico Tassinew case implementation tree | commitdiff
2007-04-02 Enrico Tassiadded some tests for cases tree | commitdiff
2007-03-10 Ferruccio Guidiadded a test for rewrite under Pi tree | commitdiff
2007-02-26 Ferruccio Guididecompose: delta-expansion of the type to eliminate... tree | commitdiff
2007-02-21 Ferruccio Guididecompose now works without premises tree | commitdiff
2007-02-08 Claudio Sacerdoti... * 'default "equality"' command changed to consider... tree | commitdiff
2007-02-06 Ferruccio Guidi- Procedural: moved in a directory on its own tree | commitdiff
2007-01-31 Claudio Sacerdoti... New test for mutual recursive definitions. tree | commitdiff
2006-12-31 Ferruccio Guidisome tests patched tree | commitdiff
2006-12-30 Ferruccio Guidi dependence to legacy/coq.ma fixed tree | commitdiff
2006-12-18 Claudio Sacerdoti... An idea to implement manifest record fields: tree | commitdiff
2006-12-01 Ferruccio Guidisome uris fixed tree | commitdiff
2006-11-30 Claudio Sacerdoti... New syntax and semantics for the rewriting steps that... tree | commitdiff
2006-11-27 Claudio Sacerdoti... auto new => auto new library in those tests that use... tree | commitdiff
2006-11-25 Enrico Tassiadded a test for the pullback stuff and the possibility... tree | commitdiff
2006-10-09 Claudio Sacerdoti... One auto modified in an apply since auto is no longer... tree | commitdiff
2006-10-09 Claudio Sacerdoti... auto => auto new and other minor changes to make it... tree | commitdiff
2006-10-09 Claudio Sacerdoti... auto => auto new everywhere + minor updates to make... tree | commitdiff
2006-10-03 Enrico Tassireduced timeout to 100s tree | commitdiff
2006-10-03 Enrico Tassicommented out are_convertible in is_identity tree | commitdiff
2006-10-03 Claudio Sacerdoti... Removed /home/tassi from the makefile! tree | commitdiff
2006-10-02 Enrico Tassi... tree | commitdiff
2006-10-02 Enrico Tassi... tree | commitdiff
2006-10-02 Enrico Tassiadded tests for paramod tree | commitdiff
2006-10-02 Enrico Tassi... tree | commitdiff
2006-10-02 Enrico Tassiadded missing *) tree | commitdiff
2006-09-29 Enrico Tassifixed (dasabled paramod) tree | commitdiff
2006-09-29 Enrico Tassiadded tests for auto tree | commitdiff
2006-09-29 Enrico Tassimaittaprover uses another format tree | commitdiff
2006-09-29 Enrico Tassi... tree | commitdiff
2006-09-27 Claudio Sacerdoti... New bug found in disambiguation of records. tree | commitdiff
2006-09-26 Claudio Sacerdoti... Two tests used to have the same baseuri. Very bad. tree | commitdiff
2006-09-26 Claudio Sacerdoti... discriminate => destruct tree | commitdiff
2006-09-25 Claudio Sacerdoti... injection_tac and discriminate_tac now replaced by... tree | commitdiff
2006-09-25 Claudio Sacerdoti... Several bugs fixed in discriminate. tree | commitdiff
2006-09-21 Enrico Tassi... tree | commitdiff
2006-09-20 Claudio Sacerdoti... Injection now clears all intermediate results introduced. tree | commitdiff
2006-09-14 Claudio Sacerdoti... 1. Stricter controls implemented in injection. tree | commitdiff
2006-09-14 Claudio Sacerdoti... 1. added a test for injection tree | commitdiff
2006-09-05 Enrico Tassifixed coercions. composite can't occur if to funclass tree | commitdiff
2006-09-05 Enrico Tassifixed includes tree | commitdiff
2006-09-04 Enrico TassiBIG FAT COMMIT REGARDING COERCIONS: tree | commitdiff
2006-08-21 Enrico Tassi... tree | commitdiff
2006-08-21 Enrico Tassi... tree | commitdiff
2006-07-27 maiorinoAutomation enabled for declarative proofs. Cool. tree | commitdiff
2006-07-27 maiorino"that is equivalent to" and "or equivalently" implement... tree | commitdiff
2006-07-27 maiorinoAll the declarative tactics now have a more or less... tree | commitdiff
2006-07-27 maiorinoDeclarative tactics for rewriting steps, elimination... tree | commitdiff
2006-07-26 Stefano Zacchiroliadded test for reordering of goals when using the 1... tree | commitdiff
2006-07-24 Enrico Tassimore work on matitaprover (no more XML and buris are... tree | commitdiff
2006-07-24 Enrico Tassimore and more tests tree | commitdiff
2006-07-22 Enrico Tassimatitaprover tree | commitdiff
2006-07-19 Claudio Sacerdoti... Submitted a test for inferencing of dependent types. tree | commitdiff
2006-07-18 Claudio Sacerdoti... baseuri for group.ma fixed tree | commitdiff
2006-07-18 Claudio Sacerdoti... Baseuri of applys.ma fixed. tree | commitdiff
2006-07-18 Claudio Sacerdoti... legacy/coq.ma included tree | commitdiff
2006-07-18 Claudio Sacerdoti... le_inv renamed to avoid conflicts with the automaticall... tree | commitdiff
2006-07-17 Enrico Tassi... tree | commitdiff
2006-07-17 Enrico Tassievvai! tree | commitdiff
2006-07-17 Enrico Tassi... tree | commitdiff
2006-07-14 Andrea AspertiAdded the computation of max_weight. tree | commitdiff
2006-07-11 maiorinoFirst experimental version of the declarative proof... tree | commitdiff
2006-07-10 Enrico Tassi- cheanges for the new coercion stuff (including the... tree | commitdiff
2006-07-06 Enrico Tassi... tree | commitdiff
2006-07-03 Enrico Tassi/.... tree | commitdiff
2006-07-03 Enrico Tassi... tree | commitdiff
2006-06-30 Enrico Tassifix tree | commitdiff
2006-06-29 Enrico Tassi... tree | commitdiff
2006-06-28 Enrico Tassifix tree | commitdiff
2006-06-28 Enrico Tassifix tree | commitdiff
2006-06-28 Enrico Tassifix tree | commitdiff
2006-06-28 Enrico Tassifixed gzip usage tree | commitdiff
2006-06-28 Enrico Tassifix tree | commitdiff
2006-06-28 Enrico Tassinew mega spreadsheet available tree | commitdiff
2006-06-28 Enrico Tassifix tree | commitdiff
2006-06-28 Enrico Tassiadded gzip to log files tree | commitdiff
2006-06-19 Enrico Tassi... tree | commitdiff
2006-06-18 Enrico Tassifix tree | commitdiff
2006-06-16 Enrico Tassifixed tree | commitdiff
2006-06-16 Enrico Tassifixes tree | commitdiff
2006-06-16 Enrico Tassiecco le gatte da pelare tree | commitdiff
2006-06-16 Enrico Tassiadded log.120.orsay.txt and comparison tree | commitdiff
2006-06-15 Andrea Aspertisome examples of the new ApplyS tactic tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.