| 2010-07-28 |
Enrico Tassi | ... |
blob | commitdiff | raw |
| 2010-03-31 |
Andrea Asperti | Tracing mechanism for auto. Interface changed to solve... |
blob | commitdiff | raw | diff to current |
| 2010-01-18 |
Andrea Asperti | Number notation for NG |
blob | commitdiff | raw | diff to current |
| 2009-10-28 |
Claudio Sacerdoti... | One-shot aliases were no longer generated because of... |
blob | commitdiff | raw | diff to current |
| 2009-10-02 |
Enrico Tassi | fixed bug in coercion application, input/output swapped... |
blob | commitdiff | raw | diff to current |
| 2009-06-18 |
Claudio Sacerdoti... | Stricter type: the type now shows that disambiguation... |
blob | commitdiff | raw | diff to current |
| 2009-06-18 |
Claudio Sacerdoti... | 1) grafiteWalker removed |
blob | commitdiff | raw | diff to current |
| 2009-06-17 |
Claudio Sacerdoti... | Initial implementation of statuses using objects in... |
blob | commitdiff | raw | diff to current |
| 2009-06-16 |
Claudio Sacerdoti... | 1) unification hint now takes NG terms (as it should... |
blob | commitdiff | raw | diff to current |
| 2009-06-16 |
Claudio Sacerdoti... | 1) NCicLibrary (which is untrusted) moved after NCicUnt... |
blob | commitdiff | raw | diff to current |
| 2009-06-16 |
Claudio Sacerdoti... | FIX OF THE PREVIOUS EXPERIMENTAL COMMIT: |
blob | commitdiff | raw | diff to current |
| 2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status: |
blob | commitdiff | raw | diff to current |
| 2009-06-09 |
Enrico Tassi | termAcicContent is logic independent (despite its name... |
blob | commitdiff | raw | diff to current |
| 2009-05-18 |
Enrico Tassi | in the new kernel you can type Type[i] to mean Type_i... |
blob | commitdiff | raw | diff to current |
| 2009-04-25 |
Claudio Sacerdoti... | Lookup_in_library implemented for new objects. Basicall... |
blob | commitdiff | raw | diff to current |
| 2009-04-25 |
Claudio Sacerdoti... | It is now possible to declare new aliases using the... |
blob | commitdiff | raw | diff to current |
| 2009-04-25 |
Claudio Sacerdoti... | The translation from old aliases to new references... |
blob | commitdiff | raw | diff to current |
| 2009-04-24 |
Claudio Sacerdoti... | - Grammar for all obj commands ported to NG (let recs... |
blob | commitdiff | raw | diff to current |
| 2009-04-24 |
Claudio Sacerdoti... | Quick&dirty implementation of neqd: |
blob | commitdiff | raw | diff to current |
| 2009-04-22 |
Wilmer Ricciotti | New command "inverter" used to generate an induction... |
blob | commitdiff | raw | diff to current |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
blob | commitdiff | raw | diff to current |
| 2009-04-01 |
Enrico Tassi | 1) mk_meta now returns also the index of the created... |
blob | commitdiff | raw | diff to current |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
blob | commitdiff | raw | diff to current |
| 2009-03-10 |
Enrico Tassi | unification hints almost ready |
blob | commitdiff | raw | diff to current |
| 2009-03-03 |
Enrico Tassi | - fixed hint generation, more hints are generated |
blob | commitdiff | raw | diff to current |
| 2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
blob | commitdiff | raw | diff to current |
| 2008-12-19 |
Enrico Tassi | more pps |
blob | commitdiff | raw | diff to current |
| 2008-12-19 |
Enrico Tassi | added unification hint |
blob | commitdiff | raw | diff to current |
| 2008-12-18 |
Claudio Sacerdoti... | New disambiguation commented out. |
blob | commitdiff | raw | diff to current |
| 2008-12-16 |
Enrico Tassi | move the printing in the right place |
blob | commitdiff | raw | diff to current |
| 2008-12-15 |
Wilmer Ricciotti | First attempt to implement unification hints. |
blob | commitdiff | raw | diff to current |
| 2008-12-12 |
Enrico Tassi | use new function to clear caches so that objects are... |
blob | commitdiff | raw | diff to current |
| 2008-12-09 |
Enrico Tassi | new disambiguatio attached with the right universe... |
blob | commitdiff | raw | diff to current |
| 2008-12-05 |
Enrico Tassi | coercions are there, but not heavily tested |
blob | commitdiff | raw | diff to current |
| 2008-12-05 |
Enrico Tassi | still commented, but benchmarks the new/old disambiguti... |
blob | commitdiff | raw | diff to current |
| 2008-12-04 |
Enrico Tassi | Fixes: |
blob | commitdiff | raw | diff to current |
| 2008-12-03 |
Claudio Sacerdoti... | The aliases and multi_aliases in the lexicon status... |
blob | commitdiff | raw | diff to current |
| 2008-11-28 |
Enrico Tassi | it works! |
blob | commitdiff | raw | diff to current |
| 2008-11-28 |
Enrico Tassi | new disambiguator almost attached |
blob | commitdiff | raw | diff to current |
| 2008-11-27 |
Enrico Tassi | New modules stack: |
blob | commitdiff | raw | diff to current |
| 2008-11-27 |
Enrico Tassi | 1. grafiteDisambiguator => multiPassDisambiguator |
blob | commitdiff | raw | diff to current |
| 2008-11-27 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2008-11-27 |
Enrico Tassi | disambiguation should not fail if the new refiner fails |
blob | commitdiff | raw | diff to current |
| 2008-11-26 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2008-11-26 |
Enrico Tassi | disambiguation even more abstracted |
blob | commitdiff | raw | diff to current |
| 2008-11-21 |
Enrico Tassi | disambiguation now returns and takes in input the subst... |
blob | commitdiff | raw | diff to current |
| 2008-11-15 |
Enrico Tassi | disambiguation can use a goal as hint for the expected... |
blob | commitdiff | raw | diff to current |
| 2008-10-17 |
Enrico Tassi | new command eval added |
blob | commitdiff | raw | diff to current |
| 2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
blob | commitdiff | raw | diff to current |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
blob | commitdiff | raw | diff to current |
| 2008-06-19 |
Claudio Sacerdoti... | 1. bug fixed in generalize_pattern: a lazy const_tac... |
blob | commitdiff | raw | diff to current |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
blob | commitdiff | raw | diff to current |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
blob | commitdiff | raw | diff to current |
| 2008-03-10 |
Claudio Sacerdoti... | Tactic reduce got rid of. Use normalize, instead. |
blob | commitdiff | raw | diff to current |
| 2008-02-26 |
Ferruccio Guidi | I added some debugging information |
blob | commitdiff | raw | diff to current |
| 2008-01-10 |
Enrico Tassi | BIG FAT WARNING: DEVELOPMENTS DIE HERE |
blob | commitdiff | raw | diff to current |
| 2007-11-14 |
Ferruccio Guidi | now destruct takes an optional list of term rather... |
blob | commitdiff | raw | diff to current |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
blob | commitdiff | raw | diff to current |
| 2007-07-04 |
Claudio Sacerdoti... | 1. "by proof" now allowed as a justification in equalit... |
blob | commitdiff | raw | diff to current |
| 2007-06-04 |
Enrico Tassi | new more flexible compose, see matita/tests/compose... |
blob | commitdiff | raw | diff to current |
| 2007-06-01 |
Enrico Tassi | new compose tactic, still undocumented. |
blob | commitdiff | raw | diff to current |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
blob | commitdiff | raw | diff to current |
| 2007-05-09 |
Ferruccio Guidi | PrimitiveTactics: intros _ now aveilable |
blob | commitdiff | raw | diff to current |
| 2007-04-20 |
Claudio Sacerdoti... | Much ado about nothing: |
blob | commitdiff | raw | diff to current |
| 2007-03-16 |
Ferruccio Guidi | elim tactic: it needs two arguments, a term as well... |
blob | commitdiff | raw | diff to current |
| 2007-03-13 |
Ferruccio Guidi | elim tactic: now takes a pattern instead of just a... |
blob | commitdiff | raw | diff to current |
| 2007-03-01 |
Enrico Zoli | "by j let x : T such that P(x)" generalized to allow... |
blob | commitdiff | raw | diff to current |
| 2007-02-21 |
Ferruccio Guidi | procedural : some improvements. |
blob | commitdiff | raw | diff to current |
| 2007-01-24 |
Ferruccio Guidi | matitaGui: some missing cases during disambiguation... |
blob | commitdiff | raw | diff to current |
| 2006-12-29 |
Ferruccio Guidi | - tactics: |
blob | commitdiff | raw | diff to current |
| 2006-12-20 |
Claudio Sacerdoti... | New declarative tactic "we proceed by cases on t to... |
blob | commitdiff | raw | diff to current |
| 2006-12-20 |
Claudio Sacerdoti... | New tactic cases (still to be documented). |
blob | commitdiff | raw | diff to current |
| 2006-12-05 |
Stefano Zacchiroli | experimental classification of disambiguation error... |
blob | commitdiff | raw | diff to current |
| 2006-11-30 |
Claudio Sacerdoti... | New syntax and semantics for the rewriting steps that... |
blob | commitdiff | raw | diff to current |
| 2006-11-29 |
Claudio Sacerdoti... | The rewritingstep declarative command now takes also... |
blob | commitdiff | raw | diff to current |
| 2006-11-23 |
Andrea Asperti | Command index added to disambiguate. |
blob | commitdiff | raw | diff to current |
| 2006-10-18 |
Claudio Sacerdoti... | - Disambiguation error exception enriched with more... |
blob | commitdiff | raw | diff to current |
| 2006-10-18 |
Claudio Sacerdoti... | Disambiguation errors now carry more information (i... |
blob | commitdiff | raw | diff to current |
| 2006-10-09 |
Claudio Sacerdoti... | applyS now receives the same parameters that auto receives. |
blob | commitdiff | raw | diff to current |
| 2006-10-03 |
Claudio Sacerdoti... | Inline command implemented. |
blob | commitdiff | raw | diff to current |
| 2006-09-27 |
Claudio Sacerdoti... | Initial work on setoids: |
blob | commitdiff | raw | diff to current |
| 2006-09-25 |
Claudio Sacerdoti... | injection_tac and discriminate_tac now replaced by... |
blob | commitdiff | raw | diff to current |
| 2006-08-29 |
Ferruccio Guidi | - new tactic subst removes simple non recursive equalit... |
blob | commitdiff | raw | diff to current |
| 2006-08-28 |
Ferruccio Guidi | - Level-1: some fixes to the extraction procedure |
blob | commitdiff | raw | diff to current |
| 2006-07-27 |
maiorino | Declarative tactics for rewriting steps, elimination... |
blob | commitdiff | raw | diff to current |
| 2006-07-27 |
maiorino | New declarative commands (ast, pretty-printing and... |
blob | commitdiff | raw | diff to current |
| 2006-07-22 |
Enrico Tassi | matitaprover |
blob | commitdiff | raw | diff to current |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Quit (unused) removed. |
blob | commitdiff | raw | diff to current |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Print (unused) removed. |
blob | commitdiff | raw | diff to current |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Search_pat and GrafiteAst.Search_term (both... |
blob | commitdiff | raw | diff to current |
| 2006-07-11 |
maiorino | First experimental version of the declarative proof... |
blob | commitdiff | raw | diff to current |
| 2006-06-29 |
Claudio Sacerdoti... | Demodulate used to be a reduction_kind and it used... |
blob | commitdiff | raw | diff to current |
| 2006-06-28 |
Ferruccio Guidi | - "linear" flag added to lapply (automatic clearing) |
blob | commitdiff | raw | diff to current |
| 2006-06-21 |
Enrico Tassi | added the geniric |
blob | commitdiff | raw | diff to current |
| 2006-06-15 |
Andrea Asperti | Apply-Silvie tactic added! |
blob | commitdiff | raw | diff to current |
| 2006-05-09 |
Enrico Tassi | types2006 patch |
blob | commitdiff | raw | diff to current |
| 2006-02-08 |
Claudio Sacerdoti... | Never implemented tactics compare and decide equality... |
blob | commitdiff | raw | diff to current |
| 2006-02-03 |
Stefano Zacchiroli | - renamed ocaml/ to components/ |
blob | commitdiff | raw | diff to current |
|
projects / helm.git / history