| 2009-06-03 |
Claudio Sacerdoti... | Huge commit with several changes: |
tree | commitdiff |
| 2009-05-28 |
Ferruccio Guidi | - cicInspect: relevant nodes count updated: letin nodes... |
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-18 |
Enrico Tassi | nothing special |
tree | commitdiff |
| 2009-05-18 |
Claudio Sacerdoti... | 1) GrafiteAst.NEval => GrafiteAst.NReduce |
tree | commitdiff |
| 2009-05-11 |
Claudio Sacerdoti... | - non_punctuational_tacticals ported to NG |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-06 |
Ferruccio Guidi | - dependenciesParser: updated to new inline syntax |
tree | commitdiff |
| 2009-05-05 |
Ferruccio Guidi | - Procedural: new flag "level=n" to control the reconst... |
tree | commitdiff |
| 2009-05-05 |
Ferruccio Guidi | - hExtlib: new function "list_assoc_all" |
tree | commitdiff |
| 2009-04-29 |
Claudio Sacerdoti... | Records are now interpreted in the NG (but I am sure... |
tree | commitdiff |
| 2009-04-28 |
Enrico Tassi | huge commit in automation: |
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-25 |
Ferruccio Guidi | - matitacLib: better handling of the callbacks for... |
tree | commitdiff |
| 2009-04-24 |
Claudio Sacerdoti... | - Grammar for all obj commands ported to NG (let recs... |
tree | commitdiff |
| 2009-04-24 |
Claudio Sacerdoti... | Quick&dirty implementation of neqd: |
tree | commitdiff |
| 2009-04-22 |
Wilmer Ricciotti | New command "inverter" used to generate an induction... |
tree | commitdiff |
| 2009-04-22 |
Enrico Tassi | demodulate takes an extra argument 'all', if present... |
tree | commitdiff |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
tree | commitdiff |
| 2009-04-16 |
Claudio Sacerdoti... | The context is now parsed in the reverse (right) order. |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | we rebuilt the dependences |
tree | commitdiff |
| 2009-04-14 |
Claudio Sacerdoti... | assert_tac now takes a list of sequents and also checks... |
tree | commitdiff |
| 2009-04-14 |
Claudio Sacerdoti... | New debugging tactic nassert: |
tree | commitdiff |
| 2009-04-09 |
Enrico Tassi | added letin, still broken |
tree | commitdiff |
| 2009-04-09 |
Enrico Tassi | new tactic whd implemented |
tree | commitdiff |
| 2009-04-08 |
Enrico Tassi | generalized is half-implemented (still broken) |
tree | commitdiff |
| 2009-04-07 |
Claudio Sacerdoti... | - nrewrite ((very?) rough implementation) |
tree | commitdiff |
| 2009-04-06 |
Claudio Sacerdoti... | New tactic clear; new syntax # _; to introduce and... |
tree | commitdiff |
| 2009-04-06 |
Enrico Tassi | tactic cases works! delift clears tags |
tree | commitdiff |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic "case1_tac" that make "intro" followed by... |
tree | commitdiff |
| 2009-04-01 |
Claudio Sacerdoti... | ## prefix is now used for tinycals |
tree | commitdiff |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic intro. Syntax: "# n". |
tree | commitdiff |
| 2009-04-01 |
Enrico Tassi | added tentative elim |
tree | commitdiff |
| 2009-04-01 |
Enrico Tassi | 1) mk_meta now returns also the index of the created... |
tree | commitdiff |
| 2009-03-30 |
Enrico Tassi | tentative subst-sexpand and change |
tree | commitdiff |
| 2009-03-26 |
Enrico Tassi | new apply almost there |
tree | commitdiff |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
| 2009-03-10 |
Enrico Tassi | unification hints almost ready |
tree | commitdiff |
| 2009-03-03 |
Enrico Tassi | - fixed hint generation, more hints are generated |
tree | commitdiff |
| 2009-02-17 |
Ferruccio Guidi | - Coq/preamble: missing alias added |
tree | commitdiff |
| 2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | more pps |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | added unification hint |
tree | commitdiff |
| 2008-12-19 |
Enrico Tassi | unification hint |
tree | commitdiff |
| 2008-12-18 |
Claudio Sacerdoti... | New disambiguation commented out. |
tree | commitdiff |
| 2008-12-16 |
Enrico Tassi | move the printing in the right place |
tree | commitdiff |
| 2008-12-15 |
Wilmer Ricciotti | First attempt to implement unification hints. |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | use new function to clear caches so that objects are... |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | new disambiguatio attached with the right universe... |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | coercions are there, but not heavily tested |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | still commented, but benchmarks the new/old disambiguti... |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | Fixes: |
tree | commitdiff |
| 2008-12-03 |
Claudio Sacerdoti... | The aliases and multi_aliases in the lexicon status... |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | it works! |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | new disambiguator almost attached |
tree | commitdiff |
| 2008-11-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | New modules stack: |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | 1. grafiteDisambiguator => multiPassDisambiguator |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | disambiguation should not fail if the new refiner fails |
tree | commitdiff |
| 2008-11-26 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-26 |
Enrico Tassi | disambiguation even more abstracted |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | loc * lazy string -> (loc * string) lazy |
tree | commitdiff |
| 2008-11-21 |
Enrico Tassi | disambiguation now returns and takes in input the subst... |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | disambiguation can use a goal as hint for the expected... |
tree | commitdiff |
| 2008-11-14 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-12 |
Enrico Tassi | exported disambiguate_thing |
tree | commitdiff |
| 2008-10-17 |
Enrico Tassi | new command eval added |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | more push/pop to avoid confusion with imperative data... |
tree | commitdiff |
| 2008-09-02 |
Claudio Sacerdoti... | Uri ending in '' were not accepted. Fixed. |
tree | commitdiff |
| 2008-08-25 |
Ferruccio Guidi | bug fix in inline syntax |
tree | commitdiff |
| 2008-08-21 |
Ferruccio Guidi | basic support for imposed flavour in procedural object... |
tree | commitdiff |
| 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 |
| next |
projects / helm.git / history