| 2009-07-14 |
denes | Fixed Option type error (OCaml bug) |
blob | commitdiff | raw |
| 2009-07-10 |
Enrico Tassi | initial implementation of coercion composition |
blob | commitdiff | raw | diff to current |
| 2009-07-10 |
Claudio Sacerdoti... | Bug fixed (missing ctx) + comment added. |
blob | commitdiff | raw | diff to current |
| 2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :... |
blob | commitdiff | raw | diff to current |
| 2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical |
blob | commitdiff | raw | diff to current |
| 2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
blob | commitdiff | raw | diff to current |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
blob | commitdiff | raw | diff to current |
| 2009-06-23 |
Enrico Tassi | undo/serialization for universes implemented |
blob | commitdiff | raw | diff to current |
| 2009-06-23 |
Claudio Sacerdoti... | 1) NCicTypechecker.typecheck_obj removed, since it... |
blob | commitdiff | raw | diff to current |
| 2009-06-19 |
Claudio Sacerdoti... | Estatus finally merged into the global status using... |
blob | commitdiff | raw | diff to current |
| 2009-06-19 |
Claudio Sacerdoti... | Useless GrafiteTypes.get_baseuri removed. |
blob | commitdiff | raw | diff to current |
| 2009-06-19 |
Claudio Sacerdoti... | More statuses converted to objects. |
blob | commitdiff | raw | diff to current |
| 2009-06-18 |
Enrico Tassi | debug pps removed |
blob | commitdiff | raw | diff to current |
| 2009-06-18 |
Claudio Sacerdoti... | Objects are now used to represent also the tactic status. |
blob | commitdiff | raw | diff to current |
| 2009-06-18 |
denes | Added ntry and nassumption tactics |
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 |
Enrico Tassi | avoid fixing non-recursive terms |
blob | commitdiff | raw | diff to current |
| 2009-06-16 |
Enrico Tassi | we fix recursive object reference with the correct... |
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 | EXPERIMENTAL COMMIT (by CSC,actuall :-) |
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-15 |
Enrico Tassi | part of last commit |
blob | commitdiff | raw | diff to current |
| 2009-06-09 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2009-06-05 |
denes | First tests for paramodulation (pretty printer, unifica... |
blob | commitdiff | raw | diff to current |
| 2009-06-05 |
Claudio Sacerdoti... | The kernel _must_ check the correctness of the height... |
blob | commitdiff | raw | diff to current |
| 2009-06-03 |
Claudio Sacerdoti... | Huge commit with several changes: |
blob | commitdiff | raw | diff to current |
| 2009-05-28 |
Ferruccio Guidi | - cicInspect: relevant nodes count updated: letin nodes... |
blob | commitdiff | raw | diff to current |
| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser: |
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-05-18 |
Claudio Sacerdoti... | 1) GrafiteAst.NEval => GrafiteAst.NReduce |
blob | commitdiff | raw | diff to current |
| 2009-05-11 |
Claudio Sacerdoti... | - non_punctuational_tacticals ported to NG |
blob | commitdiff | raw | diff to current |
| 2009-05-08 |
Claudio Sacerdoti... | 1) better implementation of NObj that now calls recursi... |
blob | commitdiff | raw | diff to current |
| 2009-05-05 |
Enrico Tassi | - pretty printer made robust in face of list_nth |
blob | commitdiff | raw | diff to current |
| 2009-04-28 |
Enrico Tassi | huge commit in automation: |
blob | commitdiff | raw | diff to current |
| 2009-04-26 |
Claudio Sacerdoti... | The backward compatible management of aliases for NG... |
blob | commitdiff | raw | diff to current |
| 2009-04-25 |
Claudio Sacerdoti... | It is now possible for commands processed by grafiteEng... |
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-16 |
Enrico Tassi | Universe is used only locally to tactics/ |
blob | commitdiff | raw | diff to current |
| 2009-04-14 |
Claudio Sacerdoti... | assert_tac now takes a list of sequents and also checks... |
blob | commitdiff | raw | diff to current |
| 2009-04-14 |
Claudio Sacerdoti... | New debugging tactic nassert: |
blob | commitdiff | raw | diff to current |
| 2009-04-09 |
Enrico Tassi | added letin, still broken |
blob | commitdiff | raw | diff to current |
| 2009-04-09 |
Enrico Tassi | new tactic whd implemented |
blob | commitdiff | raw | diff to current |
| 2009-04-08 |
Enrico Tassi | generalized is half-implemented (still broken) |
blob | commitdiff | raw | diff to current |
| 2009-04-07 |
Claudio Sacerdoti... | - nrewrite ((very?) rough implementation) |
blob | commitdiff | raw | diff to current |
| 2009-04-06 |
Enrico Tassi | tactic cases works! delift clears tags |
blob | commitdiff | raw | diff to current |
| 2009-04-02 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic "case1_tac" that make "intro" followed by... |
blob | commitdiff | raw | diff to current |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic intro. Syntax: "# n". |
blob | commitdiff | raw | diff to current |
| 2009-04-01 |
Enrico Tassi | added tentative elim |
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-30 |
Enrico Tassi | tentative subst-sexpand and change |
blob | commitdiff | raw | diff to current |
| 2009-03-26 |
Enrico Tassi | new apply almost there |
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-01-13 |
Enrico Tassi | many changes regarding coercions: |
blob | commitdiff | raw | diff to current |
| 2008-12-19 |
Enrico Tassi | added 'unification hint command to add a term to the... |
blob | commitdiff | raw | diff to current |
| 2008-11-28 |
Ferruccio Guidi | ng_disambiguation ng_kernel ng_refiner disambiguation... |
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-09-26 |
Enrico Tassi | iremoved call to auto |
blob | commitdiff | raw | diff to current |
| 2008-09-26 |
Enrico Tassi | lazy proof term to increase sharing and decrease memory... |
blob | commitdiff | raw | diff to current |
| 2008-09-10 |
Enrico Tassi | reverted auto experiment |
blob | commitdiff | raw | diff to current |
| 2008-09-10 |
Enrico Tassi | AGAIN A TEST |
blob | commitdiff | raw | diff to current |
| 2008-09-10 |
Enrico Tassi | COMMIT TO JUST RUN A BENCH, SHOULD BE REVERTED ASAP... |
blob | commitdiff | raw | diff to current |
| 2008-09-09 |
Enrico Tassi | some work to make tries "printable", fixed comparison... |
blob | commitdiff | raw | diff to current |
| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info... |
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-04-22 |
Enrico Tassi | oblivion ugraph everywhere outside the kernel |
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-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-13 |
Ferruccio Guidi | - ProofEngineHelpers: namer_of moved to GrafiteEngine |
blob | commitdiff | raw | diff to current |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
blob | commitdiff | raw | diff to current |
| 2007-11-02 |
Ferruccio Guidi | - tacticals: new tactical ifs added: uses thens where... |
blob | commitdiff | raw | diff to current |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
blob | commitdiff | raw | diff to current |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
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-23 |
Claudio Sacerdoti... | Yet another patch to LibraryClean. |
blob | commitdiff | raw | diff to current |
| 2007-05-17 |
Enrico Tassi | added a (for the moment) dummy field _subst to Proofeng... |
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-04-20 |
Claudio Sacerdoti... | Interface of the argument to Continuationals.Make great... |
blob | commitdiff | raw | diff to current |
| 2007-04-19 |
Claudio Sacerdoti... | EXPERIMENTAL and _INCOMPLETE_ COMMIT: |
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 |
| 2007-01-10 |
Ferruccio Guidi | attributes now in the proof status: commit 2 |
blob | commitdiff | raw | diff to current |
| next |
projects / helm.git / history