]> matita.cs.unibo.it Git - helm.git/history - helm/software
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Added problems from CASC 208
[helm.git] / helm / software /
2009-05-05 Andrea Aspertiautobatch by tree | commitdiff
2009-05-01 Ferruccio Guidi- librarian: 3 bugs fixed in the building system: tree | commitdiff
2009-04-30 Enrico Tassirun check_if_goal_is_solved on all goals (active+passive) tree | commitdiff
2009-04-30 Matthias PuechAdded an option --enable-annot to the configure to... tree | commitdiff
2009-04-30 Andrea AspertiMinor changes pro-automation tree | commitdiff
2009-04-30 Andrea AspertiAdded a passive table tree | commitdiff
2009-04-30 Andrea AspertiCalling paramodulation instead of demod_all tree | commitdiff
2009-04-29 Claudio Sacerdoti... Refinement of inductive type implemented. tree | commitdiff
2009-04-29 Ferruccio Guidi- procedural: bugfix in "Barendregt convention" test tree | commitdiff
2009-04-29 Enrico Tassi... tree | commitdiff
2009-04-29 Enrico Tassicall paramod instead of solve_Rewrite tree | commitdiff
2009-04-29 Enrico Tassino typing tree | commitdiff
2009-04-29 Enrico Tassimany checks guarded with if Utils.debug_metas tree | commitdiff
2009-04-29 Claudio Sacerdoti... Records are now interpreted in the NG (but I am sure... tree | commitdiff
2009-04-28 Claudio Sacerdoti... Inductive definitions are now interpreted (but records... tree | commitdiff
2009-04-28 Claudio Sacerdoti... Last commit by Ferruccio reverted since it breaks the... tree | commitdiff
2009-04-28 Ferruccio GuidicicNotationUtil: in fresh_name_generator, "\eta" replac... tree | commitdiff
2009-04-28 Enrico Tassidepenalization of smart apply inside auto, that is... tree | commitdiff
2009-04-28 Enrico Tassifixed bug, demodulation was keeping results not strictl... tree | commitdiff
2009-04-28 Enrico Tassihuge commit in automation: tree | commitdiff
2009-04-27 Ferruccio GuidimatitacLib: bugfix in .moo generation tree | commitdiff
2009-04-26 Claudio Sacerdoti... The backward compatible management of aliases for NG... tree | commitdiff
2009-04-25 Claudio Sacerdoti... It is now possible for commands processed by grafiteEng... tree | commitdiff
2009-04-25 Claudio Sacerdoti... Lookup_in_library implemented for new objects. Basicall... tree | commitdiff
2009-04-25 Claudio Sacerdoti... It is now possible to declare new aliases using the... tree | commitdiff
2009-04-25 Ferruccio Guidi- matitacLib: lexicon status and grafite status where... tree | commitdiff
2009-04-25 Claudio Sacerdoti... The translation from old aliases to new references... tree | commitdiff
2009-04-25 Claudio Sacerdoti... Apply subst implemented also for Fixpoints. tree | commitdiff
2009-04-25 Claudio Sacerdoti... Type for list_index improved. tree | commitdiff
2009-04-25 Claudio Sacerdoti... Slightly improved type for list_index. tree | commitdiff
2009-04-25 Claudio Sacerdoti... New utility function list_index (useful in many places... tree | commitdiff
2009-04-25 Claudio Sacerdoti... Better error message. tree | commitdiff
2009-04-25 Claudio Sacerdoti... Debug option reverted. tree | commitdiff
2009-04-25 Ferruccio Guidi- matitacLib: better handling of the callbacks for... tree | commitdiff
2009-04-24 Claudio Sacerdoti... - Grammar for all obj commands ported to NG (let recs... tree | commitdiff
2009-04-24 Claudio Sacerdoti... Quick&dirty implementation of neqd: tree | commitdiff
2009-04-22 Ferruccio Guidi- transcript: we have now two styles of mma's from... tree | commitdiff
2009-04-22 Wilmer Ricciottisyntax colouring for inverters tree | commitdiff
2009-04-22 Wilmer RicciottiDisabled debug prints in the inversion principle. tree | commitdiff
2009-04-22 Wilmer RicciottiNew command "inverter" used to generate an induction... tree | commitdiff
2009-04-22 Enrico Tassidemodulate takes an extra argument 'all', if present... tree | commitdiff
2009-04-21 Ferruccio Guidi- MatitaMisc: we factorized here the function out_pream... tree | commitdiff
2009-04-21 Enrico Tassifixed last file restricting auto tables tree | commitdiff
2009-04-20 Enrico Tassi- init_cache_and_tables rewritten using the automation_... tree | commitdiff
2009-04-20 Claudio Sacerdoti... Bug fixed: variable capture in previous commit prevente... tree | commitdiff
2009-04-17 Claudio Sacerdoti... Some improvements. tree | commitdiff
2009-04-17 Claudio Sacerdoti... ... tree | commitdiff
2009-04-16 Ferruccio GuidiProcedural: we corrected two errors about the handling... tree | commitdiff
2009-04-16 Claudio Sacerdoti... Bug: let-ins are always automatically folded! tree | commitdiff
2009-04-16 Claudio Sacerdoti... ... tree | commitdiff
2009-04-16 Claudio Sacerdoti... test/a.ma => tests/ng_tactics.ma, with nassert here... tree | commitdiff
2009-04-16 Claudio Sacerdoti... Replaced long, bugged implementation of letin-tac with... tree | commitdiff
2009-04-16 Claudio Sacerdoti... Added ppterm. tree | commitdiff
2009-04-16 Claudio Sacerdoti... The context is now parsed in the reverse (right) order. tree | commitdiff
2009-04-16 Claudio Sacerdoti... ... tree | commitdiff
2009-04-16 Enrico TassiUniverse is used only locally to tactics/ tree | commitdiff
2009-04-16 Enrico Tassiadded an exception tree | commitdiff
2009-04-15 Ferruccio Guidi- transcript: bugfix tree | commitdiff
2009-04-14 Ferruccio Guidiwe rebuilt the dependences tree | commitdiff
2009-04-14 Ferruccio Guidi- Procedural: generation of "exact" is now complete tree | commitdiff
2009-04-14 Claudio Sacerdoti... Trick: the refiner always subst-expands the outtype... tree | commitdiff
2009-04-14 Claudio Sacerdoti... Bug fixed in two lines + 5 lines of comment. tree | commitdiff
2009-04-14 Claudio Sacerdoti... assert_tac now takes a list of sequents and also checks... tree | commitdiff
2009-04-14 Claudio Sacerdoti... New debugging tactic nassert: tree | commitdiff
2009-04-12 Claudio Sacerdoti... Semantic selection back again (but no semantic cut... tree | commitdiff
2009-04-12 Claudio Sacerdoti... Match is now rendered as best as possible. tree | commitdiff
2009-04-10 Claudio Sacerdoti... The sequent viewer now considers the context to render... tree | commitdiff
2009-04-09 Ferruccio Guidi- character: we adjusted some "autobatch" parameters tree | commitdiff
2009-04-09 Claudio Sacerdoti... The substitution is now taken in account when printing... tree | commitdiff
2009-04-09 Enrico Tassiadded letin, still broken tree | commitdiff
2009-04-09 Enrico Tassi... tree | commitdiff
2009-04-09 Enrico Tassinew tactic whd implemented tree | commitdiff
2009-04-09 Enrico Tassi- change implemented in 4 lines tree | commitdiff
2009-04-09 Enrico Tassi- generalize finished tree | commitdiff
2009-04-09 Enrico Tassi?_OS1 := C[ ?_IN ] tree | commitdiff
2009-04-09 Enrico Tassifixed modules order tree | commitdiff
2009-04-09 Enrico Tassiminor fixes tree | commitdiff
2009-04-09 Enrico Tassi... tree | commitdiff
2009-04-09 Claudio Sacerdoti... ... tree | commitdiff
2009-04-09 Claudio Sacerdoti... + Chain NCic.term -> content -> presentation very... tree | commitdiff
2009-04-08 Claudio Sacerdoti... Just to make it compile again. tree | commitdiff
2009-04-08 Enrico Tassigeneralized is half-implemented (still broken) tree | commitdiff
2009-04-08 Enrico TassiAnalizyng the inductive type of the eliminated term and tree | commitdiff
2009-04-07 Claudio Sacerdoti... - nrewrite ((very?) rough implementation) tree | commitdiff
2009-04-07 Claudio Sacerdoti... - more progress towards generalize, but I am stuck now tree | commitdiff
2009-04-07 Enrico Tassi- select_tac honors the hypotheses pattern when require... tree | commitdiff
2009-04-07 Enrico Tassiselect honors the substitution tree | commitdiff
2009-04-06 Claudio Sacerdoti... New tactic clear; new syntax # _; to introduce and... tree | commitdiff
2009-04-06 Claudio Sacerdoti... ... tree | commitdiff
2009-04-06 Enrico Tassitactic cases works! delift clears tags tree | commitdiff
2009-04-06 Enrico Tassieta-contraction was made on the wrong term tree | commitdiff
2009-04-06 Enrico Tassiunification: tree | commitdiff
2009-04-06 Enrico Tassibetter error message tree | commitdiff
2009-04-06 Enrico Tassiadded one exception tree | commitdiff
2009-04-06 Ferruccio Guidi- external quantification removed (will be reintroduced... tree | commitdiff
2009-04-06 Ferruccio Guidilimits: reorganized and attached to nightly tests ... tree | commitdiff
2009-04-06 Enrico Tassisnapshot tree | commitdiff
2009-04-05 Ferruccio Guidi- Procedural: now we generate the exact tactic (in... tree | commitdiff
2009-04-02 Enrico Tassi... tree | commitdiff
2009-04-02 Enrico TassiNew file nTacStatus to: tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.