]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2009-04-15 Ferruccio Guidi- transcript: bugfix
2009-04-14 Ferruccio Guidiwe rebuilt the dependences
2009-04-14 Ferruccio Guidi- Procedural: generation of "exact" is now complete
2009-04-14 Claudio Sacerdoti... Trick: the refiner always subst-expands the outtype...
2009-04-14 Claudio Sacerdoti... Bug fixed in two lines + 5 lines of comment.
2009-04-14 Claudio Sacerdoti... assert_tac now takes a list of sequents and also checks...
2009-04-14 Claudio Sacerdoti... New debugging tactic nassert:
2009-04-12 Claudio Sacerdoti... Semantic selection back again (but no semantic cut...
2009-04-12 Claudio Sacerdoti... Match is now rendered as best as possible.
2009-04-10 Claudio Sacerdoti... The sequent viewer now considers the context to render...
2009-04-09 Ferruccio Guidi- character: we adjusted some "autobatch" parameters
2009-04-09 Claudio Sacerdoti... The substitution is now taken in account when printing...
2009-04-09 Enrico Tassiadded letin, still broken
2009-04-09 Enrico Tassi...
2009-04-09 Enrico Tassinew tactic whd implemented
2009-04-09 Enrico Tassi- change implemented in 4 lines
2009-04-09 Enrico Tassi- generalize finished
2009-04-09 Enrico Tassi?_OS1 := C[ ?_IN ]
2009-04-09 Enrico Tassifixed modules order
2009-04-09 Enrico Tassiminor fixes
2009-04-09 Enrico Tassi...
2009-04-09 Claudio Sacerdoti... ...
2009-04-09 Claudio Sacerdoti... + Chain NCic.term -> content -> presentation very...
2009-04-08 Claudio Sacerdoti... Just to make it compile again.
2009-04-08 Enrico Tassigeneralized is half-implemented (still broken)
2009-04-08 Enrico TassiAnalizyng the inductive type of the eliminated term and
2009-04-07 Claudio Sacerdoti... - nrewrite ((very?) rough implementation)
2009-04-07 Claudio Sacerdoti... - more progress towards generalize, but I am stuck now
2009-04-07 Enrico Tassi- select_tac honors the hypotheses pattern when require...
2009-04-07 Enrico Tassiselect honors the substitution
2009-04-06 Claudio Sacerdoti... New tactic clear; new syntax # _; to introduce and...
2009-04-06 Claudio Sacerdoti... ...
2009-04-06 Enrico Tassitactic cases works! delift clears tags
2009-04-06 Enrico Tassieta-contraction was made on the wrong term
2009-04-06 Enrico Tassiunification:
2009-04-06 Enrico Tassibetter error message
2009-04-06 Enrico Tassiadded one exception
2009-04-06 Ferruccio Guidi- external quantification removed (will be reintroduced...
2009-04-06 Ferruccio Guidilimits: reorganized and attached to nightly tests ...
2009-04-06 Enrico Tassisnapshot
2009-04-05 Ferruccio Guidi- Procedural: now we generate the exact tactic (in...
2009-04-02 Enrico Tassi...
2009-04-02 Enrico TassiNew file nTacStatus to:
2009-04-02 Enrico Tassiadded analyse_indty
2009-04-01 Claudio Sacerdoti... New tactic "case1_tac" that make "intro" followed by...
2009-04-01 Claudio Sacerdoti... ...
2009-04-01 Claudio Sacerdoti... ## prefix is now used for tinycals
2009-04-01 Claudio Sacerdoti... New tactic intro. Syntax: "# n".
2009-04-01 Enrico Tassiadded tentative elim
2009-04-01 Enrico Tassi1) mk_meta now returns also the index of the created...
2009-04-01 Enrico Tassiremoved spurious "
2009-03-30 Enrico Tassitentative subst-sexpand and change
2009-03-30 Enrico Tassi...
2009-03-27 Enrico Tassimore comments
2009-03-27 Enrico Tassiexec and distribute implemented
2009-03-26 Enrico Tassinew apply almost there
2009-03-26 Enrico Tassi...
2009-03-26 Enrico Tassi...
2009-03-25 Enrico Tassinew tactics are almost ready
2009-03-19 Claudio Sacerdoti... ...
2009-03-19 Stefano Zacchiroliadd Homepage field
2009-03-19 Stefano Zacchiroliset package section to "ocaml"
2009-03-19 Stefano Zacchiroliadd missing ${misc:Depends}, thanks lintian!
2009-03-19 Stefano Zacchirolirelease to unstable
2009-03-19 Stefano Zacchirolidebian/*.in: more abstract substvars
2009-03-19 Stefano Zacchirolidebian/rules: use ocaml.mk as a CDBS "rules" snippet
2009-03-19 Stefano Zacchirolirefresh build-dependencies for the transition
2009-03-16 Enrico Tassiadded mactions, the three can now be collapsed to fit...
2009-03-16 Andrea AspertiNew parameters for applyS: 10 20.
2009-03-16 Andrea AspertiAdapted to new applyS.
2009-03-16 Andrea AspertiAdded a property.
2009-03-12 Claudio Sacerdoti... More details on the proof.
2009-03-12 Claudio Sacerdoti... New algorithm based on in-place modification of the...
2009-03-11 Ferruccio GuidimatitacLib: Gc.compact added after the compilation...
2009-03-11 Ferruccio GuidiProcedural: id tactics are not counted, ie they are...
2009-03-11 Ferruccio Guidibug fix + better obj flavour guessing via inner sorts
2009-03-11 Ferruccio Guidithe level 1 reconstruction procedure is now in Procedural1
2009-03-11 Ferruccio Guidi....
2009-03-11 Ferruccio Guidinew dependences
2009-03-11 Enrico Tassiunification hints with recursive calls do work!
2009-03-11 Enrico Tassiadded margin option to the pp
2009-03-11 Enrico Tassimore examples
2009-03-10 Enrico Tassiunificatiom hints with premises
2009-03-10 Ferruccio Guidiadded some commented debugging instructions :)
2009-03-10 Enrico Tassiunification hints almost ready
2009-03-10 Enrico Tassinotation ++
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-03-09 Enrico Tassi...
2009-03-06 Claudio Sacerdoti... Minor improvements in pretty-printing.
2009-03-05 Claudio Sacerdoti... New version: only new nodes are normalized; moreover...
2009-03-03 Enrico Tassi- fixed hint generation, more hints are generated
2009-03-02 Claudio Sacerdoti... ...
2009-03-02 Claudio Sacerdoti... New version.
2009-03-02 Claudio Sacerdoti... New version.
2009-03-02 Claudio Sacerdoti... New version.
2009-03-02 Claudio Sacerdoti... New version.
2009-03-02 Claudio Sacerdoti... New version.
2009-03-02 Claudio Sacerdoti... New version.
2009-03-02 Claudio Sacerdoti... New version.
next