]> matita.cs.unibo.it Git - helm.git/history - helm/software/matita
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
Procedural: higher-order unification needs a lot of hints !!
[helm.git] / helm / software / matita /
2009-05-28 Ferruccio Guidi- cicInspect: relevant nodes count updated: letin nodes... tree | commitdiff
2009-05-26 Claudio Sacerdoti... ... tree | commitdiff
2009-05-26 Claudio Sacerdoti... ... tree | commitdiff
2009-05-26 Andrea Aspertiremoved a call to autobatch. tree | commitdiff
2009-05-25 Enrico Tassinasty change in the lexer/parser: tree | commitdiff
2009-05-22 Ferruccio Guidibugfix in the output notation for eq tree | commitdiff
2009-05-21 Andrea Aspertiautobatch -> autobatch by tree | commitdiff
2009-05-19 Enrico Tassi... tree | commitdiff
2009-05-19 Enrico Tassiregenerated tree | commitdiff
2009-05-19 Enrico Tassisome horn+equality problems tree | commitdiff
2009-05-18 Claudio Sacerdoti... removed byte queries tree | commitdiff
2009-05-18 Enrico Tassiin the new kernel you can type Type[i] to mean Type_i... tree | commitdiff
2009-05-17 Claudio Sacerdoti... ... tree | commitdiff
2009-05-17 Enrico Tassibyte tests disabled tree | commitdiff
2009-05-14 Ferruccio Guidi- libraryObjects: new default "natural numbers" with... tree | commitdiff
2009-05-13 Ferruccio Guidiinterpretations placed right after the corresponding... tree | commitdiff
2009-05-13 Ferruccio Guidi- matitaEngine: some commands like "coercion" must... tree | commitdiff
2009-05-13 Andrea AspertiVia un'altra linea... tree | commitdiff
2009-05-13 Andrea AspertiSempre piu' breve tree | commitdiff
2009-05-12 Claudio Sacerdoti... Do we really want to generate eliminators for nested... tree | commitdiff
2009-05-12 Claudio Sacerdoti... All weakly positive types but imbricated ones are now... tree | commitdiff
2009-05-12 Ferruccio Guidi- Procedural: we now reconstruct "let H := v in t"... tree | commitdiff
2009-05-11 Claudio Sacerdoti... Some experiments in generation of elimination principles. tree | commitdiff
2009-05-11 Andrea AspertiA few lemmas about inclusion. tree | commitdiff
2009-05-11 Andrea AspertiMore automation tree | commitdiff
2009-05-08 Claudio Sacerdoti... Stupid typing error fixed. tree | commitdiff
2009-05-08 Claudio Sacerdoti... Improved tests (for left parameters and mutual recursiv... tree | commitdiff
2009-05-08 Andrea Aspertiversione automatizzata tree | commitdiff
2009-05-08 Andrea Aspertisymmetry of inequality sym_neq tree | commitdiff
2009-05-07 Ferruccio Guididocumentation for the inline command tree | commitdiff
2009-05-06 Ferruccio GuidiLAMBDA-TYPES: mma's recommitted because inline syntax... tree | commitdiff
2009-05-06 Ferruccio Guidi- cicUtil: is_sober now detects folded applications tree | commitdiff
2009-05-06 Enrico Tassiapply and auto.equational_case call saturation.solve_na... tree | commitdiff
2009-05-05 Ferruccio Guidi- hExtlib: new function "list_assoc_all" tree | commitdiff
2009-05-05 Enrico Tassimore tests tree | commitdiff
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-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 Claudio Sacerdoti... Records are now interpreted in the NG (but I am sure... 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 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... 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 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-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 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 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 Guidi- Procedural: generation of "exact" is now complete 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 Tassi... tree | commitdiff
2009-04-09 Claudio Sacerdoti... + Chain NCic.term -> content -> presentation very... 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-05 Ferruccio Guidi- Procedural: now we generate the exact tactic (in... tree | commitdiff
2009-04-02 Enrico Tassi... tree | commitdiff
2009-04-01 Claudio Sacerdoti... New tactic "case1_tac" that make "intro" followed by... tree | commitdiff
2009-04-01 Claudio Sacerdoti... ... tree | commitdiff
2009-03-26 Enrico Tassinew apply almost there tree | commitdiff
2009-03-26 Enrico Tassi... tree | commitdiff
2009-03-19 Claudio Sacerdoti... ... tree | commitdiff
2009-03-16 Enrico Tassiadded mactions, the three can now be collapsed to fit... tree | commitdiff
2009-03-16 Andrea AspertiAdapted to new applyS. tree | commitdiff
2009-03-16 Andrea AspertiAdded a property. tree | commitdiff
2009-03-12 Claudio Sacerdoti... More details on the proof. tree | commitdiff
2009-03-12 Claudio Sacerdoti... New algorithm based on in-place modification of the... tree | commitdiff
2009-03-11 Ferruccio GuidimatitacLib: Gc.compact added after the compilation... tree | commitdiff
2009-03-11 Ferruccio GuidiProcedural: id tactics are not counted, ie they are... tree | commitdiff
2009-03-11 Ferruccio Guidinew dependences tree | commitdiff
2009-03-11 Enrico Tassimore examples tree | commitdiff
2009-03-10 Ferruccio Guidiadded some commented debugging instructions :) tree | commitdiff
2009-03-10 Enrico Tassinotation ++ tree | commitdiff
2009-03-09 Enrico Tassi... tree | commitdiff
2009-03-06 Claudio Sacerdoti... Minor improvements in pretty-printing. tree | commitdiff
2009-03-05 Claudio Sacerdoti... New version: only new nodes are normalized; moreover... tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.