]> matita.cs.unibo.it Git - helm.git/history - helm/ocaml/tactics
paramodulation now compiles with ocaml 3.09 in opt mode (added -for-pack)
[helm.git] / helm / ocaml / tactics /
2006-01-08 Claudio Sacerdoti... Added $Id$ to every .ml file.
2006-01-08 Claudio Sacerdoti... Added $Id$ to the file.
2006-01-08 Claudio Sacerdoti... .cvsignore files removed (the svn:property property...
2005-12-21 Claudio Sacerdoti... Huge reorganization of matita and ocaml.
2005-12-20 Stefano Zacchirolibugfix: typo which implied using the wrong pattern
2005-12-16 Enrico Tassiregenerated
2005-12-15 marangonNew tactic: inversion.
2005-12-12 Stefano Zacchirolichanged pattern datatype:
2005-12-07 Enrico TassiBig commit to let Ferruccio try the merge_coercion...
2005-11-27 Stefano Zacchiroliremoved deadcode / fixed typos (thanks to ocaml 3.09)
2005-11-24 Stefano Zacchirolisplit non-logic level of whelp away from metadataQuery...
2005-11-24 Stefano Zacchiroliremoved the need of REQUIRES in libraries Makefile...
2005-11-24 Stefano Zacchiroliprose
2005-11-21 Claudio Sacerdoti... Invariant no longer true (since when?)
2005-11-21 Stefano Zacchirolisplit body away to ease inclusion from elsewhere
2005-11-18 Claudio Sacerdoti... Improvement/bug fix: rewriting in the hypothesis used...
2005-11-17 Claudio Sacerdoti... Comments changed/removed.
2005-11-17 Claudio Sacerdoti... "Parallel" rewriting in a list of hypothesis and in...
2005-11-17 Claudio Sacerdoti... Major code semplification and improvement:
2005-11-17 Claudio Sacerdoti... First draft implementation of rewriting in an hypothesis.
2005-11-17 Claudio Sacerdoti... New tactic rename (for now for internal usage only).
2005-11-08 Claudio Sacerdoti... Yet another semantics for simplify.
2005-11-07 Claudio Sacerdoti... Let-ins with types can now be produced.
2005-11-04 Stefano Zacchirolichanged stack entry representation
2005-10-27 Stefano Zacchirolityping errors
2005-10-26 Stefano Zacchiroliadded constraing on non-empty context for tactic applic...
2005-10-25 Claudio Sacerdoti... Semantic change: applying a tactic to the empty goal...
2005-10-25 Enrico Tassifixed lapply on new tinycals semantic
2005-10-25 Stefano Zacchirolifixed some type error
2005-10-25 Stefano Zacchirolinew tacticals
2005-10-25 Claudio Sacerdoti... Every exception that used to have type string is now...
2005-10-24 Stefano Zacchirolinew semantics, should be the basis for the (re-)impleme...
2005-10-11 Stefano Zacchiroliadded goals_of_proof
2005-10-10 Stefano Zacchiroli- added stack frame tagging
2005-10-09 Claudio Sacerdoti... More informative exceptions raised.
2005-10-06 Stefano Zacchirolichanged functor interface, now based on proofs instead...
2005-10-06 Stefano Zacchiroli- better naming
2005-10-06 Stefano Zacchirolifirst check in of continuationals implementation
2005-10-03 Stefano Zacchirolirestated ...
2005-09-30 Stefano Zacchiroli- fixed some metasenv issues
2005-09-30 Stefano Zacchirolifixed some (more) typos
2005-09-30 Stefano Zacchirolifixed some typos
2005-09-30 Stefano Zacchirolicontinuationals semantics: first draft
2005-09-29 Alberto Griggionon-default equalities in equations_for_goal
2005-09-26 Alberto Griggionew signature of auto_tac, with a new optional argument...
2005-09-26 Alberto Griggioadded apply_tac_verbose_with_subst, returning a Cic...
2005-09-23 Claudio Sacerdoti... New module HMysql (to abstract over Mysql and make...
2005-09-21 Claudio Sacerdoti... All the debug_print are now lazy.
2005-09-19 Claudio Sacerdoti... Profiling code commented out.
2005-09-15 Stefano Zacchirolibugfix in discriminate: now works also with inductive...
2005-09-13 Enrico Tassiwe have to pass back lastmeta and not newmeta (newmeta...
2005-09-13 Claudio Sacerdoti... Two bugs fixed in the apply tactic:
2005-09-08 Stefano Zacchiroliremoved some debugging prints
2005-09-08 Stefano Zacchiroliimplemented lazy disambiguation of tactics arguments...
2005-09-05 Claudio Sacerdoti... Unfold tactic generalized to perform zeta-reduction.
2005-09-05 Claudio Sacerdoti... locate_in_* functions generalized to handle equalities...
2005-09-05 Enrico Tassifix generation of applications of applications.
2005-09-05 Enrico Tassiadded @raise in comment (and source)
2005-09-05 Claudio Sacerdoti... New strategy for let-in unfolding (aka zeta reduction...
2005-08-30 Claudio Sacerdoti... Bug fixed: "cic:/dummy_i" is an invalid URI (that used...
2005-07-28 Claudio Sacerdoti... 1. ProofEngineHelpers.locate_in_term, ProofEngineHelper...
2005-07-28 Claudio Sacerdoti... Bug fixed: unfold used to work iff the term to unfold...
2005-07-28 Claudio Sacerdoti... Bug fixed: locate_term_in_conjecture used to raise...
2005-07-28 Claudio Sacerdoti... New tactic unfold.
2005-07-26 Claudio Sacerdoti... locate_in_term generalized to locate_in_conjecture
2005-07-26 Claudio Sacerdoti... Comments added.
2005-07-26 Claudio Sacerdoti... Implementation of locate_in finished.
2005-07-26 Stefano Zacchirolidraft version of locate_in_term
2005-07-25 Claudio Sacerdoti... ...
2005-07-22 Alberto Griggioadded optional "paramodulation" parameter to auto to...
2005-07-21 Alberto Griggioif paramodulation fails, go on with the normal auto...
2005-07-21 Alberto Griggiointegration with paramodulation
2005-07-19 Ferruccio Guidithe decompose tactic is now working
2005-07-12 Andrea AspertiAdded a function equations_for_goal similar to signatur...
2005-07-09 Claudio Sacerdoti... Some terms were processed in the wrong context.
2005-07-09 Claudio Sacerdoti... Generalize ported to the new select up to unification.
2005-07-08 Claudio Sacerdoti... Replace is now working again and it is able to match...
2005-07-08 Claudio Sacerdoti... Elim generalized: the term to eliminate is now saturate...
2005-07-08 Claudio Sacerdoti... Cosmetic changes: a piece of code replaced with a pre...
2005-07-08 Claudio Sacerdoti... Bug fixed: metavariables generated by the saturation...
2005-07-08 Claudio Sacerdoti... The fix and cofix cases of the select were not finished...
2005-07-08 Claudio Sacerdoti... 1. PrimitiveTactics.new_metasenv_for_apply changed...
2005-07-07 Enrico Tassiapply_tac now catches TypeChecerFailure and raises...
2005-07-07 Enrico Tassifixed auto when the context has some deleted hypothesis
2005-07-07 Enrico Tassitab -> spaces
2005-07-06 Claudio Sacerdoti... Bug fixed: "intros n" should fail when there are less...
2005-07-06 Claudio Sacerdoti... Fixed a bug in the "do" tactical that made it diverge.
2005-07-06 Claudio Sacerdoti... 1. tactical "try_tacticals" renamed to "first"
2005-07-06 Enrico Tassiclear now fails if the hypothesys doesnt exist, and...
2005-07-06 Enrico Tassinow it doesn't try to apply a cleared hypothesis
2005-07-06 Claudio Sacerdoti... Some precisations on a few comments by Ferruccio.
2005-07-05 Ferruccio Guidiname specifications added for elim_intros, elim_intros_...
2005-07-05 Ferruccio Guidiid ;-) and lapply patched
2005-07-04 Claudio Sacerdoti... New command default "foo" uri1 ... urin
2005-07-04 Claudio Sacerdoti... All the tactics have been ported to use the objects...
2005-07-04 Claudio Sacerdoti... Comestic changes.
2005-07-04 Claudio Sacerdoti... Cosmetic changes.
2005-07-02 Claudio Sacerdoti... All the equalityTactics have now been ported to use...
2005-07-01 Claudio Sacerdoti... replace tactic reimplemented.
2005-07-01 Claudio Sacerdoti... pattern_of function reimplemented. Now it takes a term...
next