]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
incomplete snapshot ....
[helm.git] / helm / ocaml / tactics /
2005-10-03 Stefano Zacchirolirestated ... tree | commitdiff
2005-09-30 Stefano Zacchiroli- fixed some metasenv issues tree | commitdiff
2005-09-30 Stefano Zacchirolifixed some (more) typos tree | commitdiff
2005-09-30 Stefano Zacchirolifixed some typos tree | commitdiff
2005-09-30 Stefano Zacchirolicontinuationals semantics: first draft tree | commitdiff
2005-09-29 Alberto Griggionon-default equalities in equations_for_goal tree | commitdiff
2005-09-26 Alberto Griggionew signature of auto_tac, with a new optional argument... tree | commitdiff
2005-09-26 Alberto Griggioadded 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 Zacchirolibugfix in discriminate: now works also with inductive... tree | commitdiff
2005-09-13 Enrico Tassiwe 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 Zacchiroliremoved some debugging prints tree | commitdiff
2005-09-08 Stefano Zacchiroliimplemented 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 Tassifix generation of applications of applications. tree | commitdiff
2005-09-05 Enrico Tassiadded @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 Zacchirolidraft version of locate_in_term tree | commitdiff
2005-07-25 Claudio Sacerdoti... ... tree | commitdiff
2005-07-22 Alberto Griggioadded optional "paramodulation" parameter to auto to... tree | commitdiff
2005-07-21 Alberto Griggioif paramodulation fails, go on with the normal auto... tree | commitdiff
2005-07-21 Alberto Griggiointegration with paramodulation tree | commitdiff
2005-07-19 Ferruccio Guidithe decompose tactic is now working tree | commitdiff
2005-07-12 Andrea AspertiAdded 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 Tassiapply_tac now catches TypeChecerFailure and raises... tree | commitdiff
2005-07-07 Enrico Tassifixed auto when the context has some deleted hypothesis tree | commitdiff
2005-07-07 Enrico Tassitab -> 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 Tassiclear now fails if the hypothesys doesnt exist, and... tree | commitdiff
2005-07-06 Enrico Tassinow 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 Guidiname specifications added for elim_intros, elim_intros_... tree | commitdiff
2005-07-05 Ferruccio Guidiid ;-) 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 Guidilapply 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 Tassiremoved 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 Guidilapply reimplemented using letin_tac tree | commitdiff
2005-06-28 Ferruccio Guidilapply 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 Tassisupport 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
2005-06-27 Enrico Tassi1) moved select and pattern_of from cicUtil to proofEng... tree | commitdiff
2005-06-27 Enrico Tassifixed LApply pretty printing tree | commitdiff
2005-06-25 Ferruccio Guidifirst working (?) version of lapply tree | commitdiff
2005-06-25 Ferruccio Guidifirs wrking (?) version of lapply tree | commitdiff
2005-06-24 Ferruccio Guidilapply tactic continued tree | commitdiff
2005-06-24 Enrico Tassinew implementation (due to paths). tree | commitdiff
2005-06-24 Enrico Tassistupid rename tree | commitdiff
2005-06-24 Enrico Tassinow we use rplace_lifting_csc since the what must NOT... tree | commitdiff
2005-06-24 Claudio Sacerdoti... New implementation of experimental_hint/auto (called... tree | commitdiff
2005-06-24 Claudio Sacerdoti... New functions UriManager.uri_is_var, UriManager.uri_is_con. tree | commitdiff
2005-06-24 Claudio Sacerdoti... Asts generalized: a lot of tactics where restricted... tree | commitdiff
2005-06-23 Enrico TassiMuch simpler (and slightly more performant) implementat... tree | commitdiff
2005-06-23 Claudio Sacerdoti... Tactic generalize ported to patterns and activated... tree | commitdiff
2005-06-17 Enrico Tassiadded support for goal patterns tree | commitdiff
2005-06-17 Claudio Sacerdoti... more strings to UriManager.uri tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.