]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tactics
Trick: the refiner always subst-expands the outtype, so that the beta-redex
[helm.git] / helm / software / components / tactics /
2009-03-25 Enrico Tassinew tactics are almost ready
2009-03-16 Andrea AspertiNew parameters for applyS: 10 20.
2009-03-10 Andrea AspertiA version of applyS with bounded iterations of given_cl...
2009-03-10 Andrea AspertiRemoved the context from the metasenv to avoid trivial...
2009-02-15 Enrico Tassicommented some printings
2009-02-12 Andrea Aspertierrata corrige.
2009-02-12 Andrea AspertiFixed a problem of lifting.
2009-02-03 Enrico Tassicase tactic first tries with a simple outtype and then...
2009-01-15 Enrico Tassi- name mangling changed, added __ to separate additiona...
2009-01-13 Enrico Tassimany changes regarding coercions:
2009-01-08 Enrico Tassimore composites to make all happy!
2008-11-27 Enrico Tassi1. grafiteDisambiguator => multiPassDisambiguator
2008-11-16 Enrico Tassiremoved some printings
2008-11-16 Enrico Tassiremoved some printings
2008-11-07 Andrea Aspertidebug=false
2008-11-07 Andrea AspertiSignature_of has been closed with respect to constructors.
2008-11-07 Andrea AspertiThe signature in "retrieve equations" must be extended...
2008-11-06 Enrico Tassithe passive set and passive list are expected to have...
2008-11-05 Enrico Tassinew internal flags for auto:
2008-11-05 Enrico Tassiduplicate entry in menv avoided
2008-11-04 Andrea AspertiCalling unification instead of matching when checking...
2008-11-03 Enrico Tassiremoved prerr_endline
2008-11-03 Enrico Tassidebug=false
2008-11-01 Enrico Tassiadded lazy
2008-10-29 Andrea AspertiPropagation of changes in paramodulation.
2008-10-29 Andrea AspertiExported a couple of functions.
2008-10-29 Andrea AspertiAdded a in_universe function
2008-10-29 Andrea Aspertipropagation of changes in other paramodulation files.
2008-10-29 Andrea AspertiNew demod function working for arbitary goals.
2008-10-29 Andrea AspertiEnforcing the disjoint invariant between metasenvs.
2008-10-29 Andrea AspertiMain change: added a parameter to build_equality_proof...
2008-09-26 Enrico Tassiauto was compiraing lazy proof terms with = ... fixed
2008-09-26 Enrico Tassilazy proof term to increase sharing and decrease memory...
2008-09-19 Enrico Tassimore abstract discrimination tree
2008-09-19 Enrico Tassibetter abstraction to allow 1 discrimination tree imple...
2008-09-19 Enrico TassiRevised discrimination tree implementation:
2008-09-19 Andrea AspertiA temporary patch to demodulation theorem.
2008-09-09 Enrico Tassisome work to make tries "printable", fixed comparison...
2008-08-28 Ferruccio GuidicicDischarge: new module for discharging the explicit...
2008-07-07 Enrico Tassisimplified coercDb implementation with additional info...
2008-07-04 Ferruccio Guidi- Procedural: bug fix in rendering the application...
2008-07-02 Ferruccio Guidi- new tactic applyP for use in the *P*rocedural script...
2008-07-02 Enrico Tassicalculation of the sort user to choose the rewriting...
2008-06-19 Claudio Sacerdoti... 1. bug fixed in generalize_pattern: a lazy const_tac...
2008-06-08 Claudio Sacerdoti... Bug fixed: wrong default pattern for generalize.
2008-06-08 Claudio Sacerdoti... Hypotheses patterns for elim implemented. No more need...
2008-05-30 Enrico TassiCProp hierarchy is there!
2008-05-26 Enrico Tassinew, more rigid syntax, for auto_params affecting the...
2008-05-26 Enrico TassiUniverse.key was not used to index terms, but was used...
2008-05-24 Enrico Tassiorder of goals changes, open ones are preferred to...
2008-04-22 Enrico Tassioblivion ugraph everywhere outside the kernel
2008-04-01 Enrico Tassibetter check for progress
2008-04-01 Enrico Tassiprogress made better, still not perfect
2008-04-01 Enrico Tassiadded to rewrite a check to effectively do something...
2008-04-01 Enrico Tassiadded some comments, but the samentics of many function...
2008-03-20 Enrico Tassichanged auto_tac params type and all derivate tactics...
2008-03-19 Claudio Sacerdoti... prerr_endline => debug_print
2008-03-12 Enrico Tassifixed implicit
2008-03-11 Claudio Sacerdoti... Very experimental commit: the type of the source is...
2008-03-10 Claudio Sacerdoti... Bad hack to avoid failure of conversion (unfolding...
2008-03-10 Claudio Sacerdoti... ...
2008-03-10 Claudio Sacerdoti... Tactic reduce got rid of. Use normalize, instead.
2008-03-10 Claudio Sacerdoti... An unimplemented case of clearbody is now implemented.
2008-03-09 Claudio Sacerdoti... Performance improvement: let-ins should always be pushe...
2008-01-10 Enrico TassiBIG FAT WARNING: DEVELOPMENTS DIE HERE
2007-12-04 Enrico Tassiif parameter type is given, this assert is false
2007-11-17 Enrico Tassimoved to pkg-ocaml-maint
2007-11-16 Enrico Tassi...
2007-11-16 Enrico Tassicompose tactic restore and added nocomposites keyword
2007-11-15 Enrico Tassiremoved ugly prerr_endline
2007-11-14 Ferruccio Guidinow destruct takes an optional list of term rather...
2007-11-13 Ferruccio Guidi- ProofEngineHelpers: namer_of moved to GrafiteEngine
2007-11-12 Ferruccio Guidi- destruct tactic: automatic simplification in case...
2007-11-08 Enrico Tassiplease, commit files with debug=false otherwise the...
2007-11-07 Ferruccio Guidi- bug fix in destruct
2007-11-06 Ferruccio Guidinew implementation of the destruct tactic,
2007-11-04 Claudio Sacerdoti... All exported names are now qualified. This avoids the...
2007-11-02 Ferruccio Guidi- tacticals: new tactical ifs added: uses thens where...
2007-10-30 Ferruccio Guidibetter implementation of if_
2007-10-29 Ferruccio Guidi- destruct: core of subst tactic implemented,
2007-10-28 Claudio Sacerdoti... Pretty-printing of "match ... with" pattern syntax...
2007-10-26 Enrico Tassirebuilt
2007-10-25 Ferruccio Guidibug fix in injection e relocate term
2007-10-24 Ferruccio Guidibug fix in injection: we have to recur on the generated...
2007-10-24 Ferruccio Guidiwe revisited the implementation of the destruct tactic...
2007-10-24 Ferruccio Guidi- new function for general relocation of local referenc...
2007-10-12 Claudio Sacerdoti... Move to OCaml 3.10. Requires debian packages from unsta...
2007-10-11 Claudio Sacerdoti... Old inversion bug fixed: it used to work only on the...
2007-10-09 Enrico Tassiadded patch to allow i,j,k: skip and *: skip
2007-09-08 Enrico Tassithe order of abstraction is now correct, but there...
2007-09-08 Enrico Tassijust a Pcre expression fixed, nothing real
2007-09-07 Enrico Tassidisabled coercions when refining paramod proofs (attemt...
2007-09-04 Claudio Sacerdoti... Composition of coercions with arity > 0 is now implemen...
2007-09-04 Claudio Sacerdoti... 1. composition of coercions with saturations > 0 is...
2007-08-30 Claudio Sacerdoti... Coercions are now generalized to the general form
2007-08-23 Claudio Sacerdoti... Bug fixed: the initial metasenv used in the two tactic...
2007-08-22 Claudio Sacerdoti... select now works correctly even if multiple hypotheses...
2007-08-21 Claudio Sacerdoti... "obtain H E1=E2 by proof" is now working
2007-07-26 Enrico Tassilittle bug in coercion generation found. it use to...
2007-07-25 Enrico Tassireverted previous fix
next