]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita
\ldots are now used in nelim and ncases
[helm.git] / helm / software / matita /
2009-06-11 denesActive goals are now demodulated after selecting a...
2009-06-11 Ferruccio Guidi- applyTransformation: bugfix in the rendering of records
2009-06-11 Ferruccio Guidi- some depend files fixed
2009-06-10 Ferruccio Guidi- library/list/list.ma: unused code commented
2009-06-10 Enrico Tassi1) added simplification of actives w.r.t. selected
2009-06-09 Ferruccio Guidi- Procedural: more support for the Debug inline option...
2009-06-09 Enrico Tassisnapshot
2009-06-06 Claudio Sacerdoti... Previous commit reverted, as explained in that log.
2009-06-06 Claudio Sacerdoti... This commit restores the ids_to_father_ids table.
2009-06-05 Ferruccio Guidi- Procedural convertible rewrites in the conclusion...
2009-06-05 denesFirst tests for paramodulation (pretty printer, unifica...
2009-06-05 Wilmer Ricciotti- replaced part1a/defn with the version based on induct...
2009-06-05 Claudio Sacerdoti... 1) the home button of CicBrowser now works also for NG
2009-06-03 Ferruccio Guidi- boxPp: added missing spaces
2009-06-03 Wilmer RicciottiUpdate, using induction/inversion.
2009-06-03 Andrea Aspertinot_to_not
2009-06-03 Claudio Sacerdoti... New test for NG notation.
2009-06-03 Claudio Sacerdoti... Huge commit with several changes:
2009-06-01 Andrea AspertiThis works for me
2009-05-29 Wilmer RicciottiPOPLmark part 1a using the de Bruijn encoding.
2009-05-29 Ferruccio Guidi- cicNotationParser: added extra space to TeX control...
2009-05-28 Ferruccio Guidi- cicInspect: relevant nodes count updated: letin nodes...
2009-05-26 Claudio Sacerdoti... ...
2009-05-26 Claudio Sacerdoti... ...
2009-05-26 Andrea Aspertiremoved a call to autobatch.
2009-05-25 Enrico Tassinasty change in the lexer/parser:
2009-05-22 Ferruccio Guidibugfix in the output notation for eq
2009-05-21 Andrea Aspertiautobatch -> autobatch by
2009-05-19 Enrico Tassi...
2009-05-19 Enrico Tassiregenerated
2009-05-19 Enrico Tassisome horn+equality problems
2009-05-18 Claudio Sacerdoti... removed byte queries
2009-05-18 Enrico Tassiin the new kernel you can type Type[i] to mean Type_i...
2009-05-17 Claudio Sacerdoti... ...
2009-05-17 Enrico Tassibyte tests disabled
2009-05-14 Ferruccio Guidi- libraryObjects: new default "natural numbers" with...
2009-05-13 Ferruccio Guidiinterpretations placed right after the corresponding...
2009-05-13 Ferruccio Guidi- matitaEngine: some commands like "coercion" must...
2009-05-13 Andrea AspertiVia un'altra linea...
2009-05-13 Andrea AspertiSempre piu' breve
2009-05-12 Claudio Sacerdoti... Do we really want to generate eliminators for nested...
2009-05-12 Claudio Sacerdoti... All weakly positive types but imbricated ones are now...
2009-05-12 Ferruccio Guidi- Procedural: we now reconstruct "let H := v in t"...
2009-05-11 Claudio Sacerdoti... Some experiments in generation of elimination principles.
2009-05-11 Andrea AspertiA few lemmas about inclusion.
2009-05-11 Andrea AspertiMore automation
2009-05-08 Claudio Sacerdoti... Stupid typing error fixed.
2009-05-08 Claudio Sacerdoti... Improved tests (for left parameters and mutual recursiv...
2009-05-08 Andrea Aspertiversione automatizzata
2009-05-08 Andrea Aspertisymmetry of inequality sym_neq
2009-05-07 Ferruccio Guididocumentation for the inline command
2009-05-06 Ferruccio GuidiLAMBDA-TYPES: mma's recommitted because inline syntax...
2009-05-06 Ferruccio Guidi- cicUtil: is_sober now detects folded applications
2009-05-06 Enrico Tassiapply and auto.equational_case call saturation.solve_na...
2009-05-05 Ferruccio Guidi- hExtlib: new function "list_assoc_all"
2009-05-05 Enrico Tassimore tests
2009-05-05 Andrea Aspertiautobatch by
2009-05-01 Ferruccio Guidi- librarian: 3 bugs fixed in the building system:
2009-04-30 Enrico Tassirun check_if_goal_is_solved on all goals (active+passive)
2009-04-30 Matthias PuechAdded an option --enable-annot to the configure to...
2009-04-30 Andrea AspertiMinor changes pro-automation
2009-04-29 Claudio Sacerdoti... Refinement of inductive type implemented.
2009-04-29 Ferruccio Guidi- procedural: bugfix in "Barendregt convention" test
2009-04-29 Enrico Tassi...
2009-04-29 Claudio Sacerdoti... Records are now interpreted in the NG (but I am sure...
2009-04-28 Claudio Sacerdoti... Last commit by Ferruccio reverted since it breaks the...
2009-04-28 Ferruccio GuidicicNotationUtil: in fresh_name_generator, "\eta" replac...
2009-04-28 Enrico Tassihuge commit in automation:
2009-04-27 Ferruccio GuidimatitacLib: bugfix in .moo generation
2009-04-26 Claudio Sacerdoti... The backward compatible management of aliases for NG...
2009-04-25 Claudio Sacerdoti... Lookup_in_library implemented for new objects. Basicall...
2009-04-25 Claudio Sacerdoti... It is now possible to declare new aliases using the...
2009-04-25 Ferruccio Guidi- matitacLib: lexicon status and grafite status where...
2009-04-25 Claudio Sacerdoti... The translation from old aliases to new references...
2009-04-25 Ferruccio Guidi- matitacLib: better handling of the callbacks for...
2009-04-24 Claudio Sacerdoti... - Grammar for all obj commands ported to NG (let recs...
2009-04-22 Ferruccio Guidi- transcript: we have now two styles of mma's from...
2009-04-22 Wilmer Ricciottisyntax colouring for inverters
2009-04-22 Enrico Tassidemodulate takes an extra argument 'all', if present...
2009-04-21 Ferruccio Guidi- MatitaMisc: we factorized here the function out_pream...
2009-04-21 Enrico Tassifixed last file restricting auto tables
2009-04-20 Enrico Tassi- init_cache_and_tables rewritten using the automation_...
2009-04-20 Claudio Sacerdoti... Bug fixed: variable capture in previous commit prevente...
2009-04-17 Claudio Sacerdoti... Some improvements.
2009-04-17 Claudio Sacerdoti... ...
2009-04-16 Ferruccio GuidiProcedural: we corrected two errors about the handling...
2009-04-16 Claudio Sacerdoti... Bug: let-ins are always automatically folded!
2009-04-16 Claudio Sacerdoti... ...
2009-04-16 Claudio Sacerdoti... test/a.ma => tests/ng_tactics.ma, with nassert here...
2009-04-16 Enrico TassiUniverse is used only locally to tactics/
2009-04-16 Enrico Tassiadded an exception
2009-04-15 Ferruccio Guidi- transcript: bugfix
2009-04-14 Ferruccio Guidi- Procedural: generation of "exact" is now complete
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 Tassi...
2009-04-09 Claudio Sacerdoti... + Chain NCic.term -> content -> presentation very...
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 ...
next