]> matita.cs.unibo.it Git - helm.git/history - matita/tests
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
tagging rc-1
[helm.git] / matita / tests /
2007-11-13 Ferruccio Guidipreviously hidden simplifications (in old destruct... tree | commitdiff
2007-11-07 Ferruccio Guidi- bug fix in destruct tree | commitdiff
2007-11-06 Ferruccio Guidinew implementation of the destruct tactic, tree | commitdiff
2007-10-15 Claudio Sacerdoti... Dead code clean-up. tree | commitdiff
2007-10-15 Claudio Sacerdoti... The behaviour of autobatch paramodulation has changed. tree | commitdiff
2007-10-15 Claudio Sacerdoti... natural number => Coq natural number tree | commitdiff
2007-10-15 Claudio Sacerdoti... natural number => Coq natural number tree | commitdiff
2007-10-15 Claudio Sacerdoti... natural number => Coq natural number tree | commitdiff
2007-10-15 Claudio Sacerdoti... Wrong test patched. tree | commitdiff
2007-10-15 Claudio Sacerdoti... natural number => Coq natural number tree | commitdiff
2007-10-15 Claudio Sacerdoti... discriminate.ma => destruct.ma tree | commitdiff
2007-10-15 Claudio Sacerdoti... Spurious code removed. tree | commitdiff
2007-10-15 Claudio Sacerdoti... natural number => Coq natural number tree | commitdiff
2007-10-15 Claudio Sacerdoti... Old wrong code to avoid old bug fixed. tree | commitdiff
2007-10-15 Claudio Sacerdoti... Stupid bug fixed. tree | commitdiff
2007-10-15 Claudio Sacerdoti... auto ==> autobatch tree | commitdiff
2007-10-15 Claudio Sacerdoti... Stupid bug fixed (I deleted "assumption a" by error). tree | commitdiff
2007-10-15 Claudio Sacerdoti... auto => autobatch tree | commitdiff
2007-10-15 Claudio Sacerdoti... auto => autobatch tree | commitdiff
2007-09-10 Claudio Sacerdoti... This test shows one of the few cases were Matita is... tree | commitdiff
2007-09-08 Enrico Tassibetter test for church numerals tree | commitdiff
2007-09-08 Enrico TassiFull specification of find. Added notation for If_Then_... tree | commitdiff
2007-09-07 Enrico Tassi1. fix_arity fixed: the code is totally wrong and this... tree | commitdiff
2007-09-07 Enrico TassiThis cast now works! tree | commitdiff
2007-09-07 Enrico Tassifixed propagation under Fix/Lambda/Case of coercions... tree | commitdiff
2007-09-06 Enrico Tassi... tree | commitdiff
2007-09-05 Claudio Sacerdoti... added fix case tree | commitdiff
2007-09-04 Claudio Sacerdoti... A test for propagation of coercions (that open new... tree | commitdiff
2007-08-31 Claudio Sacerdoti... alpha conversion to avoid case-insensitivity of MySql... tree | commitdiff
2007-08-31 Claudio Sacerdoti... baseuri changed tree | commitdiff
2007-08-30 Enrico Tassitests for coercions under lambdas tree | commitdiff
2007-07-26 Enrico Tassiauto -> autobatch tree | commitdiff
2007-07-26 Enrico Tassimore stuff about coercions tree | commitdiff
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
next
Unnamed repository; edit this file 'description' to name the repository.