| 2010-03-31 |
Wilmer Ricciotti | Added test file for inversion in ng matita. |
tree | commitdiff |
| 2010-02-25 |
Wilmer Ricciotti | Minimal example in Z showing a problem in the nnormaliz... |
tree | commitdiff |
| 2009-12-01 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-11-16 |
Wilmer Ricciotti | Implementation of ndestruct tactic (including destructi... |
tree | commitdiff |
| 2009-10-20 |
Claudio Sacerdoti... | - Bug fixed: some assert failure were just failures... |
tree | commitdiff |
| 2009-10-20 |
Wilmer Ricciotti | ... |
tree | commitdiff |
| 2009-10-13 |
Wilmer Ricciotti | Experimental scripts for nth-order rewriting principles. |
tree | commitdiff |
| 2009-10-11 |
Enrico Tassi | auto with intro |
tree | commitdiff |
| 2009-10-08 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-09-23 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | Since I guess the divergence bug is fixed, I activate... |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | more work on coercions composition |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | claudio, please have a look at this |
tree | commitdiff |
| 2009-07-08 |
Enrico Tassi | removed useless universes |
tree | commitdiff |
| 2009-07-08 |
Enrico Tassi | import of a sample for cosimo |
tree | commitdiff |
| 2009-06-29 |
Enrico Tassi | removed a maybe diverging test |
tree | commitdiff |
| 2009-06-26 |
Andrea Asperti | test for deep subsumption added |
tree | commitdiff |
| 2009-06-18 |
Enrico Tassi | callbacks were taking in input a status bu were not... |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (part B, by CSC :-): |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | EXPERIMENTAL COMMIT (by CSC,actuall :-) |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status: |
tree | commitdiff |
| 2009-06-11 |
denes | Active goals are now demodulated after selecting a... |
tree | commitdiff |
| 2009-06-10 |
Enrico Tassi | 1) added simplification of actives w.r.t. selected |
tree | commitdiff |
| 2009-06-09 |
Enrico Tassi | snapshot |
tree | commitdiff |
| 2009-06-05 |
denes | First tests for paramodulation (pretty printer, unifica... |
tree | commitdiff |
| 2009-06-03 |
Claudio Sacerdoti... | New test for NG notation. |
tree | commitdiff |
| 2009-05-26 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-26 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser: |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | in the new kernel you can type Type[i] to mean Type_i... |
tree | commitdiff |
| 2009-05-17 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-12 |
Claudio Sacerdoti... | Do we really want to generate eliminators for nested... |
tree | commitdiff |
| 2009-05-12 |
Claudio Sacerdoti... | All weakly positive types but imbricated ones are now... |
tree | commitdiff |
| 2009-05-11 |
Claudio Sacerdoti... | Some experiments in generation of elimination principles. |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | Stupid typing error fixed. |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | Improved tests (for left parameters and mutual recursiv... |
tree | commitdiff |
| 2009-05-05 |
Enrico Tassi | more tests |
tree | commitdiff |
| 2009-04-29 |
Claudio Sacerdoti... | Refinement of inductive type implemented. |
tree | commitdiff |
| 2009-04-29 |
Claudio Sacerdoti... | Records are now interpreted in the NG (but I am sure... |
tree | commitdiff |
| 2009-04-26 |
Claudio Sacerdoti... | The backward compatible management of aliases for NG... |
tree | commitdiff |
| 2009-04-25 |
Claudio Sacerdoti... | Lookup_in_library implemented for new objects. Basicall... |
tree | commitdiff |
| 2009-04-25 |
Claudio Sacerdoti... | It is now possible to declare new aliases using the... |
tree | commitdiff |
| 2009-04-25 |
Claudio Sacerdoti... | The translation from old aliases to new references... |
tree | commitdiff |
| 2009-04-24 |
Claudio Sacerdoti... | - Grammar for all obj commands ported to NG (let recs... |
tree | commitdiff |
| 2009-04-17 |
Claudio Sacerdoti... | Some improvements. |
tree | commitdiff |
| 2009-04-17 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-04-16 |
Claudio Sacerdoti... | Bug: let-ins are always automatically folded! |
tree | commitdiff |
| 2009-04-16 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-04-16 |
Claudio Sacerdoti... | test/a.ma => tests/ng_tactics.ma, with nassert here... |
tree | commitdiff |
| 2009-04-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic "case1_tac" that make "intro" followed by... |
tree | commitdiff |
| 2009-04-01 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-03-26 |
Enrico Tassi | new apply almost there |
tree | commitdiff |
| 2009-03-11 |
Enrico Tassi | more examples |
tree | commitdiff |
| 2009-03-10 |
Enrico Tassi | notation ++ |
tree | commitdiff |
| 2009-03-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-12-16 |
Enrico Tassi | hints work better now |
tree | commitdiff |
| 2008-12-15 |
Wilmer Ricciotti | Some changes to the pullback test, for debugging |
tree | commitdiff |
| 2008-11-14 |
Enrico Tassi | test 4 luo |
tree | commitdiff |
| 2008-09-19 |
Enrico Tassi | fixed |
tree | commitdiff |
| 2008-09-18 |
Enrico Tassi | fixed script |
tree | commitdiff |
| 2008-08-23 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-21 |
Ferruccio Guidi | we implemented the support for generating ma files... |
tree | commitdiff |
| 2008-07-16 |
Ferruccio Guidi | Procedural: some comments added in the generated script |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | Hypotheses patterns for elim implemented. No more need... |
tree | commitdiff |
| 2008-06-03 |
Enrico Tassi | xxx |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-04-24 |
Enrico Tassi | added coinductive example |
tree | commitdiff |
| 2008-04-15 |
Claudio Sacerdoti... | added sample of guarded by in which coq is stronger |
tree | commitdiff |
| 2008-04-03 |
Enrico Tassi | added ugly test showing many many bugs in the current... |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | new semantics for 'by t' |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | removed pointless test |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | I believe that auto paramodulation does not try to |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | added library option to auto |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | letins are no more unfolded, we do that by hand |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | letin are no longer unfolded thus coercions not propaga... |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | Files committed by Enrico (a mistake, I suppose) removed. |
tree | commitdiff |
| 2008-01-10 |
Enrico Tassi | BIG FAT WARNING: DEVELOPMENTS DIE HERE |
tree | commitdiff |
| 2007-11-13 |
Ferruccio Guidi | previously hidden simplifications (in old destruct... |
tree | commitdiff |
| 2007-11-07 |
Ferruccio Guidi | - bug fix in destruct |
tree | commitdiff |
| 2007-11-06 |
Ferruccio Guidi | new 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 |
| next |
projects / helm.git / history