2005-11-04 |
Stefano Zacchiroli | changed stack entry representation |
tree | commitdiff |
2005-10-27 |
Stefano Zacchiroli | typing errors |
tree | commitdiff |
2005-10-26 |
Stefano Zacchiroli | added constraing on non-empty context for tactic applic... |
tree | commitdiff |
2005-10-25 |
Claudio Sacerdoti... | Semantic change: applying a tactic to the empty goal... |
tree | commitdiff |
2005-10-25 |
Enrico Tassi | fixed lapply on new tinycals semantic |
tree | commitdiff |
2005-10-25 |
Stefano Zacchiroli | fixed some type error |
tree | commitdiff |
2005-10-25 |
Stefano Zacchiroli | new tacticals |
tree | commitdiff |
2005-10-25 |
Claudio Sacerdoti... | Every exception that used to have type string is now... |
tree | commitdiff |
2005-10-24 |
Stefano Zacchiroli | new semantics, should be the basis for the (re-)impleme... |
tree | commitdiff |
2005-10-11 |
Stefano Zacchiroli | added goals_of_proof |
tree | commitdiff |
2005-10-10 |
Stefano Zacchiroli | - added stack frame tagging |
tree | commitdiff |
2005-10-09 |
Claudio Sacerdoti... | More informative exceptions raised. |
tree | commitdiff |
2005-10-06 |
Stefano Zacchiroli | changed functor interface, now based on proofs instead... |
tree | commitdiff |
2005-10-06 |
Stefano Zacchiroli | - better naming |
tree | commitdiff |
2005-10-06 |
Stefano Zacchiroli | first check in of continuationals implementation |
tree | commitdiff |
2005-10-03 |
Stefano Zacchiroli | restated ... |
tree | commitdiff |
2005-09-30 |
Stefano Zacchiroli | - fixed some metasenv issues |
tree | commitdiff |
2005-09-30 |
Stefano Zacchiroli | fixed some (more) typos |
tree | commitdiff |
2005-09-30 |
Stefano Zacchiroli | fixed some typos |
tree | commitdiff |
2005-09-30 |
Stefano Zacchiroli | continuationals semantics: first draft |
tree | commitdiff |
2005-09-29 |
Alberto Griggio | non-default equalities in equations_for_goal |
tree | commitdiff |
2005-09-26 |
Alberto Griggio | new signature of auto_tac, with a new optional argument... |
tree | commitdiff |
2005-09-26 |
Alberto Griggio | added apply_tac_verbose_with_subst, returning a Cic... |
tree | commitdiff |
2005-09-23 |
Claudio Sacerdoti... | New module HMysql (to abstract over Mysql and make... |
tree | commitdiff |
2005-09-21 |
Claudio Sacerdoti... | All the debug_print are now lazy. |
tree | commitdiff |
2005-09-19 |
Claudio Sacerdoti... | Profiling code commented out. |
tree | commitdiff |
2005-09-15 |
Stefano Zacchiroli | bugfix in discriminate: now works also with inductive... |
tree | commitdiff |
2005-09-13 |
Enrico Tassi | we have to pass back lastmeta and not newmeta (newmeta... |
tree | commitdiff |
2005-09-13 |
Claudio Sacerdoti... | Two bugs fixed in the apply tactic: |
tree | commitdiff |
2005-09-08 |
Stefano Zacchiroli | removed some debugging prints |
tree | commitdiff |
2005-09-08 |
Stefano Zacchiroli | implemented lazy disambiguation of tactics arguments... |
tree | commitdiff |
2005-09-05 |
Claudio Sacerdoti... | Unfold tactic generalized to perform zeta-reduction. |
tree | commitdiff |
2005-09-05 |
Claudio Sacerdoti... | locate_in_* functions generalized to handle equalities... |
tree | commitdiff |
2005-09-05 |
Enrico Tassi | fix generation of applications of applications. |
tree | commitdiff |
2005-09-05 |
Enrico Tassi | added @raise in comment (and source) |
tree | commitdiff |
2005-09-05 |
Claudio Sacerdoti... | New strategy for let-in unfolding (aka zeta reduction... |
tree | commitdiff |
2005-08-30 |
Claudio Sacerdoti... | Bug fixed: "cic:/dummy_i" is an invalid URI (that used... |
tree | commitdiff |
2005-07-28 |
Claudio Sacerdoti... | 1. ProofEngineHelpers.locate_in_term, ProofEngineHelper... |
tree | commitdiff |
2005-07-28 |
Claudio Sacerdoti... | Bug fixed: unfold used to work iff the term to unfold... |
tree | commitdiff |
2005-07-28 |
Claudio Sacerdoti... | Bug fixed: locate_term_in_conjecture used to raise... |
tree | commitdiff |
2005-07-28 |
Claudio Sacerdoti... | New tactic unfold. |
tree | commitdiff |
2005-07-26 |
Claudio Sacerdoti... | locate_in_term generalized to locate_in_conjecture |
tree | commitdiff |
2005-07-26 |
Claudio Sacerdoti... | Comments added. |
tree | commitdiff |
2005-07-26 |
Claudio Sacerdoti... | Implementation of locate_in finished. |
tree | commitdiff |
2005-07-26 |
Stefano Zacchiroli | draft version of locate_in_term |
tree | commitdiff |
2005-07-25 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2005-07-22 |
Alberto Griggio | added optional "paramodulation" parameter to auto to... |
tree | commitdiff |
2005-07-21 |
Alberto Griggio | if paramodulation fails, go on with the normal auto... |
tree | commitdiff |
2005-07-21 |
Alberto Griggio | integration with paramodulation |
tree | commitdiff |
2005-07-19 |
Ferruccio Guidi | the decompose tactic is now working |
tree | commitdiff |
2005-07-12 |
Andrea Asperti | Added a function equations_for_goal similar to signatur... |
tree | commitdiff |
2005-07-09 |
Claudio Sacerdoti... | Some terms were processed in the wrong context. |
tree | commitdiff |
2005-07-09 |
Claudio Sacerdoti... | Generalize ported to the new select up to unification. |
tree | commitdiff |
2005-07-08 |
Claudio Sacerdoti... | Replace is now working again and it is able to match... |
tree | commitdiff |
2005-07-08 |
Claudio Sacerdoti... | Elim generalized: the term to eliminate is now saturate... |
tree | commitdiff |
2005-07-08 |
Claudio Sacerdoti... | Cosmetic changes: a piece of code replaced with a pre... |
tree | commitdiff |
2005-07-08 |
Claudio Sacerdoti... | Bug fixed: metavariables generated by the saturation... |
tree | commitdiff |
2005-07-08 |
Claudio Sacerdoti... | The fix and cofix cases of the select were not finished... |
tree | commitdiff |
2005-07-08 |
Claudio Sacerdoti... | 1. PrimitiveTactics.new_metasenv_for_apply changed... |
tree | commitdiff |
2005-07-07 |
Enrico Tassi | apply_tac now catches TypeChecerFailure and raises... |
tree | commitdiff |
2005-07-07 |
Enrico Tassi | fixed auto when the context has some deleted hypothesis |
tree | commitdiff |
2005-07-07 |
Enrico Tassi | tab -> spaces |
tree | commitdiff |
2005-07-06 |
Claudio Sacerdoti... | Bug fixed: "intros n" should fail when there are less... |
tree | commitdiff |
2005-07-06 |
Claudio Sacerdoti... | Fixed a bug in the "do" tactical that made it diverge. |
tree | commitdiff |
2005-07-06 |
Claudio Sacerdoti... | 1. tactical "try_tacticals" renamed to "first" |
tree | commitdiff |
2005-07-06 |
Enrico Tassi | clear now fails if the hypothesys doesnt exist, and... |
tree | commitdiff |
2005-07-06 |
Enrico Tassi | now it doesn't try to apply a cleared hypothesis |
tree | commitdiff |
2005-07-06 |
Claudio Sacerdoti... | Some precisations on a few comments by Ferruccio. |
tree | commitdiff |
2005-07-05 |
Ferruccio Guidi | name specifications added for elim_intros, elim_intros_... |
tree | commitdiff |
2005-07-05 |
Ferruccio Guidi | id ;-) and lapply patched |
tree | commitdiff |
2005-07-04 |
Claudio Sacerdoti... | New command default "foo" uri1 ... urin |
tree | commitdiff |
2005-07-04 |
Claudio Sacerdoti... | All the tactics have been ported to use the objects... |
tree | commitdiff |
2005-07-04 |
Claudio Sacerdoti... | Comestic changes. |
tree | commitdiff |
2005-07-04 |
Claudio Sacerdoti... | Cosmetic changes. |
tree | commitdiff |
2005-07-02 |
Claudio Sacerdoti... | All the equalityTactics have now been ported to use... |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | replace tactic reimplemented. |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | pattern_of function reimplemented. Now it takes a term... |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | The replace tactic is now working again. It can now... |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | Signature of fwdSimpl changed to get rid of a warning. |
tree | commitdiff |
2005-07-01 |
Claudio Sacerdoti... | 1. change_tac moved from PrimitiveTactics to ReductionT... |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | Signature and concrete syntax of fold fixed. |
tree | commitdiff |
2005-06-30 |
Ferruccio Guidi | lapply and fwd improved |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | The rewrite_* set of tactics is now working again.... |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | Bug fixed: a wrong lift made select unuseful when wante... |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | 1. rewrite_* and rewrite_back_* merged into one function |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | Oooops. I forgot the convertibility test that makes... |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | The tactic change is now working again. Moreover, it... |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | A bit of renaming in the code to make it more clear. |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | Obsolete comment removed. |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | Stupid bug fixed (a completely erroneous assert false... |
tree | commitdiff |
2005-06-30 |
Claudio Sacerdoti... | This commit makes ProofEngineHelpers.select reach its... |
tree | commitdiff |
2005-06-29 |
Claudio Sacerdoti... | 1. new syntax for patterns: |
tree | commitdiff |
2005-06-29 |
Enrico Tassi | removed profiling function (now a stub is used instead) |
tree | commitdiff |
2005-06-29 |
Claudio Sacerdoti... | Incredible bug of simpl fixed: the stack (in the termin... |
tree | commitdiff |
2005-06-29 |
Ferruccio Guidi | lapply reimplemented using letin_tac |
tree | commitdiff |
2005-06-28 |
Ferruccio Guidi | lapply improved |
tree | commitdiff |
2005-06-27 |
Claudio Sacerdoti... | 1. interface of replace generalized to patterns |
tree | commitdiff |
2005-06-27 |
Claudio Sacerdoti... | A few other tactics made available to matita. |
tree | commitdiff |
2005-06-27 |
Enrico Tassi | support for _ in binders, and a more coplex pattern... |
tree | commitdiff |
2005-06-27 |
Claudio Sacerdoti... | * auto_tac removed (it can be found in CVS) |
tree | commitdiff |
next |