| 2008-07-21 |
Ferruccio Guidi | we implemented the support for generating ma files... |
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-24 |
Enrico Tassi | missing file added |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | notation support fixed to parentesize in a more sane... |
tree | commitdiff |
| 2008-06-22 |
Ferruccio Guidi | - grafiteParser.ml: the callback invocation was displaced |
tree | commitdiff |
| 2008-06-20 |
Claudio Sacerdoti... | - partial implementation of pattern for case documented |
tree | commitdiff |
| 2008-06-19 |
Claudio Sacerdoti... | 1. bug fixed in generalize_pattern: a lazy const_tac... |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
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-02-26 |
Ferruccio Guidi | I added some debugging information |
tree | commitdiff |
| 2008-01-10 |
Enrico Tassi | BIG FAT WARNING: DEVELOPMENTS DIE HERE |
tree | commitdiff |
| 2007-11-16 |
Enrico Tassi | compose tactic restore and added nocomposites keyword |
tree | commitdiff |
| 2007-11-14 |
Ferruccio Guidi | now destruct takes an optional list of term rather... |
tree | commitdiff |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
tree | commitdiff |
| 2007-10-24 |
Claudio Sacerdoti... | Debugging code improved. |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-07-30 |
Enrico Tassi | added 'rewrite' option to the the hint macro. a cicBrow... |
tree | commitdiff |
| 2007-07-19 |
Claudio Sacerdoti... | map_unicode_to_tex is no longer optional and it always... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | 1. "by proof" now allowed as a justification in equalit... |
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-09 |
Ferruccio Guidi | PrimitiveTactics: intros _ now aveilable |
tree | commitdiff |
| 2007-04-26 |
Ferruccio Guidi | procedural: bug fixes |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | Much ado about nothing: |
tree | commitdiff |
| 2007-04-20 |
Enrico Tassi | developments root are now part of default inclusion... |
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-02-12 |
Ferruccio Guidi | LexiconAstPp: fixed syntax for include |
tree | commitdiff |
| 2007-02-09 |
Ferruccio Guidi | added option -dump to matitac for persistent macro... |
tree | commitdiff |
| 2007-02-06 |
Ferruccio Guidi | - Procedural: moved in a directory on its own |
tree | commitdiff |
| 2007-01-31 |
Claudio Sacerdoti... | Several bugs fixed: |
tree | commitdiff |
| 2007-01-24 |
Ferruccio Guidi | matitaGui: some missing cases during disambiguation... |
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-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-18 |
Ferruccio Guidi | Procedural: some improvements |
tree | commitdiff |
| 2006-12-12 |
Ferruccio Guidi | we parametrized CicNotationPt.obj on 'term |
tree | commitdiff |
| 2006-12-12 |
Ferruccio Guidi | we started the infrastructure for the procedural render... |
tree | commitdiff |
| 2006-12-05 |
Stefano Zacchiroli | experimental classification of disambiguation error... |
tree | commitdiff |
| 2006-11-30 |
Claudio Sacerdoti... | New syntax and semantics for the rewriting steps that... |
tree | commitdiff |
| 2006-11-30 |
Claudio Sacerdoti... | The auto parameters that can be given to a declarative... |
tree | commitdiff |
| 2006-11-29 |
Claudio Sacerdoti... | The rewritingstep declarative command now takes also... |
tree | commitdiff |
| 2006-11-29 |
Ferruccio Guidi | - decompose tactic: decomposable constants are now... |
tree | commitdiff |
| 2006-11-23 |
Andrea Asperti | Command index added to disambiguate. |
tree | commitdiff |
| 2006-10-25 |
Claudio Sacerdoti... | 1. bug fixed: Unicode characters that are not mapped... |
tree | commitdiff |
| 2006-10-18 |
Claudio Sacerdoti... | - Disambiguation error exception enriched with more... |
tree | commitdiff |
| 2006-10-18 |
Claudio Sacerdoti... | Disambiguation errors now carry more information (i... |
tree | commitdiff |
| 2006-10-13 |
Claudio Sacerdoti... | New content level representations for LetRec, Inductive... |
tree | commitdiff |
| 2006-10-09 |
Claudio Sacerdoti... | applyS now receives the same parameters that auto receives. |
tree | commitdiff |
| 2006-10-03 |
maiorino | Some declarative tactics did not allow the "done" optio... |
tree | commitdiff |
| 2006-10-03 |
Claudio Sacerdoti... | Inline command implemented. |
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-09-04 |
Claudio Sacerdoti... | Aliases are now wrote down even during the first pass. |
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-08-24 |
Ferruccio Guidi | - new legature == for \equiv used in the notation for... |
tree | commitdiff |
| 2006-07-27 |
maiorino | "that is equivalent to" and "or equivalently" implement... |
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 |
Claudio Sacerdoti... | Disambiguation passes simplified. |
tree | commitdiff |
| 2006-07-22 |
Enrico Tassi | matitaprover |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | dependeciesParsed fixed to parse URIs also in QSTRINGs |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | The dependencies parser is more robust w.r.t. to lexing... |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Quit (unused) removed. |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Print (unused) removed. |
tree | commitdiff |
| 2006-07-12 |
Claudio Sacerdoti... | GrafiteAst.Search_pat and GrafiteAst.Search_term (both... |
tree | commitdiff |
| 2006-07-11 |
maiorino | First experimental version of the declarative proof... |
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-20 |
Ferruccio Guidi | - fwd concrete syntax fixed |
tree | commitdiff |
| 2006-06-20 |
Ferruccio Guidi | - added some documentation on the fwd tatcic |
tree | commitdiff |
| 2006-06-15 |
Andrea Asperti | Apply-Silvie tactic added! |
tree | commitdiff |
| 2006-06-11 |
Ferruccio Guidi | - slight fix in lapply syntax |
tree | commitdiff |
| 2006-06-09 |
Claudio Sacerdoti... | Syntactic bug changed: t in "unfold t" must be a tactic... |
tree | commitdiff |
| 2006-06-01 |
Stefano Zacchiroli | implemented tinycals: |
tree | commitdiff |
| 2006-05-25 |
Claudio Sacerdoti... | Added debug menu item to restrict disambiguation to... |
tree | commitdiff |
| 2006-05-25 |
Claudio Sacerdoti... | Axioms are not allowed with the syntax: "axiom name... |
tree | commitdiff |
| 2006-05-16 |
Enrico Tassi | utf8_macros moved to syntax_extensions. |
tree | commitdiff |
| 2006-05-11 |
Claudio Sacerdoti... | Bugs fixed: |
tree | commitdiff |
| 2006-05-09 |
Enrico Tassi | types2006 patch |
tree | commitdiff |
| 2006-04-14 |
Enrico Tassi | multi-instances aliases are compressed to single instan... |
tree | commitdiff |
| 2006-04-13 |
Enrico Tassi | added include' to include everything but preferences... |
tree | commitdiff |
| 2006-04-12 |
Enrico Tassi | whelp locate now accepts * and ? |
tree | commitdiff |
| 2006-03-15 |
Enrico Tassi | more work for the release |
tree | commitdiff |
| 2006-02-23 |
Stefano Zacchiroli | bugfix: use utf8-aware substring function |
tree | commitdiff |
| 2006-02-23 |
Stefano Zacchiroli | Added module GrafiteWalker, which implements traversals... |
tree | commitdiff |
| next |
projects / helm.git / history