| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info... |
tree | commitdiff |
| 2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-19 |
Claudio Sacerdoti... | 1. bug fixed in generalize_pattern: a lazy const_tac... |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-04-22 |
Enrico Tassi | oblivion ugraph everywhere outside the kernel |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Tactic reduce got rid of. Use normalize, instead. |
tree | commitdiff |
| 2008-01-10 |
Enrico Tassi | BIG FAT WARNING: DEVELOPMENTS DIE HERE |
tree | commitdiff |
| 2007-11-14 |
Ferruccio Guidi | now destruct takes an optional list of term rather... |
tree | commitdiff |
| 2007-11-13 |
Ferruccio Guidi | - ProofEngineHelpers: namer_of moved to GrafiteEngine |
tree | commitdiff |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
tree | commitdiff |
| 2007-11-02 |
Ferruccio Guidi | - tacticals: new tactical ifs added: uses thens where... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
tree | commitdiff |
| 2007-06-04 |
Enrico Tassi | new more flexible compose, see matita/tests/compose... |
tree | commitdiff |
| 2007-06-01 |
Enrico Tassi | new compose tactic, still undocumented. |
tree | commitdiff |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | Yet another patch to LibraryClean. |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | added a (for the moment) dummy field _subst to Proofeng... |
tree | commitdiff |
| 2007-05-09 |
Ferruccio Guidi | PrimitiveTactics: intros _ now aveilable |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | Much ado about nothing: |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | Interface of the argument to Continuationals.Make great... |
tree | commitdiff |
| 2007-04-19 |
Claudio Sacerdoti... | EXPERIMENTAL and _INCOMPLETE_ COMMIT: |
tree | commitdiff |
| 2007-03-16 |
Ferruccio Guidi | elim tactic: it needs two arguments, a term as well... |
tree | commitdiff |
| 2007-03-13 |
Ferruccio Guidi | elim tactic: now takes a pattern instead of just a... |
tree | commitdiff |
| 2007-03-01 |
Enrico Zoli | "by j let x : T such that P(x)" generalized to allow... |
tree | commitdiff |
| 2007-02-21 |
Ferruccio Guidi | procedural : some improvements. |
tree | commitdiff |
| 2007-01-24 |
Ferruccio Guidi | matitaGui: some missing cases during disambiguation... |
tree | commitdiff |
| 2007-01-10 |
Ferruccio Guidi | attributes now in the proof status: commit 2 |
tree | commitdiff |
| 2007-01-05 |
Enrico Tassi | add_moo_content does not add a coercion statement twice |
tree | commitdiff |
| 2006-12-30 |
Claudio Sacerdoti... | Serious bug fixed: arities of coercions in the .moo... |
tree | commitdiff |
| 2006-12-29 |
Ferruccio Guidi | now we try two distinct depend files for compilation... |
tree | commitdiff |
| 2006-12-29 |
Ferruccio Guidi | - tactics: |
tree | commitdiff |
| 2006-12-22 |
Andrea Asperti | Add_moo_content modified to avoid repetitions of index... |
tree | commitdiff |
| 2006-12-20 |
Claudio Sacerdoti... | New declarative tactic "we proceed by cases on t to... |
tree | commitdiff |
| 2006-12-20 |
Claudio Sacerdoti... | New tactic cases (still to be documented). |
tree | commitdiff |
| 2006-12-05 |
Ferruccio Guidi | - components: composed coercions mus be generated with... |
tree | commitdiff |
| 2006-11-29 |
Ferruccio Guidi | - decompose tactic: decomposable constants are now... |
tree | commitdiff |
| 2006-11-29 |
Andrea Asperti | Demodulate_tac now depends on the universe |
tree | commitdiff |
| 2006-11-27 |
Claudio Sacerdoti... | Declarative language ported to new auto (with Universes). |
tree | commitdiff |
| 2006-11-27 |
Andrea Asperti | Variant are not indexed. |
tree | commitdiff |
| 2006-11-23 |
Andrea Asperti | The status has been extended with a "universe", that... |
tree | commitdiff |
| 2006-10-09 |
Claudio Sacerdoti... | applyS now receives the same parameters that auto receives. |
tree | commitdiff |
| 2006-09-27 |
Claudio Sacerdoti... | Initial work on setoids: |
tree | commitdiff |
| 2006-09-25 |
Claudio Sacerdoti... | injection_tac and discriminate_tac now replaced by... |
tree | commitdiff |
| 2006-09-04 |
Enrico Tassi | BIG FAT COMMIT REGARDING COERCIONS: |
tree | commitdiff |
| 2006-08-31 |
Ferruccio Guidi | - semantics of tactic subst allmost fixed |
tree | commitdiff |
| 2006-08-29 |
Ferruccio Guidi | - new tactic subst removes simple non recursive equalit... |
tree | commitdiff |
| 2006-08-28 |
Ferruccio Guidi | - Level-1: some fixes to the extraction procedure |
tree | commitdiff |
| 2006-07-27 |
maiorino | Automation enabled for declarative proofs. Cool. |
tree | commitdiff |
| 2006-07-27 |
maiorino | All the declarative tactics now have a more or less... |
tree | commitdiff |
| 2006-07-27 |
maiorino | Declarative tactics for rewriting steps, elimination... |
tree | commitdiff |
| 2006-07-27 |
maiorino | New declarative commands (ast, pretty-printing and... |
tree | commitdiff |
| 2006-07-24 |
Enrico Tassi | more work on matitaprover (no more XML and buris are... |
tree | commitdiff |
| 2006-07-22 |
Enrico Tassi | matitaprover |
tree | commitdiff |
| 2006-07-11 |
maiorino | First experimental version of the declarative proof... |
tree | commitdiff |
| 2006-07-10 |
Enrico Tassi | improved coercions support: |
tree | commitdiff |
| 2006-07-05 |
Enrico Tassi | bugfix to developments: |
tree | commitdiff |
| 2006-06-29 |
Claudio Sacerdoti... | Demodulate used to be a reduction_kind and it used... |
tree | commitdiff |
| 2006-06-28 |
Ferruccio Guidi | - "linear" flag added to lapply (automatic clearing) |
tree | commitdiff |
| 2006-06-27 |
Ferruccio Guidi | - decompose now runs with no arguments (operates on... |
tree | commitdiff |
| 2006-06-21 |
Enrico Tassi | added the geniric |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | Apply-Silvie tactic added! |
tree | commitdiff |
| 2006-06-01 |
Stefano Zacchiroli | implemented tinycals: |
tree | commitdiff |
| 2006-05-09 |
Enrico Tassi | types2006 patch |
tree | commitdiff |
| 2006-03-17 |
Enrico Tassi | tests are now handled with a standard Makefile that... |
tree | commitdiff |
| 2006-03-13 |
Enrico Tassi | Huge commit for the release. Includes: |
tree | commitdiff |
| 2006-03-08 |
Claudio Sacerdoti... | Debugging code removed. |
tree | commitdiff |
| 2006-02-20 |
Claudio Sacerdoti... | Stupid bug fixed. |
tree | commitdiff |
| 2006-02-20 |
Claudio Sacerdoti... | Packing of implicit coercions must be also performed... |
tree | commitdiff |
| 2006-02-15 |
Enrico Tassi | added support for "polymorphic" coercions |
tree | commitdiff |
| 2006-02-08 |
Claudio Sacerdoti... | Never implemented tactics compare and decide equality... |
tree | commitdiff |
| 2006-02-03 |
Stefano Zacchiroli | - renamed ocaml/ to components/ |
tree | commitdiff |
|
projects / helm.git / history