]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2008-12-26 Claudio Sacerdoti... Some notes by Giovanni.
2008-12-26 Claudio Sacerdoti... Some notes by Giovanni.
2008-12-24 Enrico Tassiadded some virtuals
2008-12-24 Enrico Tassibug fixed, all convertible was called without a metasenv
2008-12-22 Claudio Sacerdoti... Just copied here from formal_topologies.ma.
2008-12-22 Claudio Sacerdoti... More (ugly) work.
2008-12-22 Enrico Tassi...
2008-12-22 Enrico TassiBeginning of o-basic_topologies.
2008-12-22 Enrico TassiSome clean up.
2008-12-22 Enrico TassiConcrete Spaces defined but... they require about 20m...
2008-12-22 Enrico Tassi1 more lemma
2008-12-22 Enrico Tassione line
2008-12-22 Enrico Tassisome work
2008-12-22 Claudio Sacerdoti... ums got rid of
2008-12-21 Claudio Sacerdoti... 1) no more DAEMONS
2008-12-21 Enrico Tassimerged commits, the same proof is missing :-(
2008-12-21 Enrico Tassibleah
2008-12-21 Claudio Sacerdoti... Using the new category SET.
2008-12-21 Claudio Sacerdoti... New category SET (whose objects are setoids).
2008-12-20 Ferruccio Guidiwe started the support for naive sort inclusion
2008-12-19 Enrico Tassibetter pp of virtuals
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassimore pps
2008-12-19 Enrico Tassitype3
2008-12-19 Enrico Tassiranking hopefully fixed
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassifix exponentiation
2008-12-19 Enrico Tassigo notation go!
2008-12-19 Enrico Tassifixed, it seems the new handling of hints in some rare...
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassiadded aliases for _ and fixed greek leters thanks to...
2008-12-19 Enrico Tassibetter pps
2008-12-19 Enrico Tassihandles bad Appl
2008-12-19 Enrico Tassiadded better debug_pps and add_user_provided_unificatio...
2008-12-19 Enrico Tassi...
2008-12-19 Enrico Tassiadded unification hint
2008-12-19 Enrico Tassiunification hint
2008-12-19 Enrico Tassilambda case fixed, used to not properly use the expecte...
2008-12-19 Enrico Tassiadded 'unification hint command to add a term to the...
2008-12-19 Enrico Tassiidentity coercions are not really inserted, just used...
2008-12-19 Enrico Tassi....
2008-12-18 Claudio Sacerdoti... Stupid bug fixed: checkin the type in place of the...
2008-12-18 Claudio Sacerdoti... New disambiguation commented out.
2008-12-18 Claudio Sacerdoti... Many axioms are now proved... using many more (but...
2008-12-18 Claudio Sacerdoti... Now it compiles again.
2008-12-18 Claudio Sacerdoti... Refinement of axioms fixed. We did not check that the...
2008-12-18 Ferruccio Guidi- improved logging
2008-12-18 Enrico Tassi...
2008-12-17 Ferruccio Guidiwe started the support for the coercions "alle" and...
2008-12-17 Enrico Tassifoo overlap
2008-12-17 Enrico Tassifoo overlap
2008-12-17 Enrico Tassi....
2008-12-16 Ferruccio Guidiwe added the implicit coercion for modus tollens
2008-12-16 Enrico Tassiprevious change was causing divergence
2008-12-16 Enrico Tassihints work better now
2008-12-16 Enrico Tassihints attached
2008-12-16 Enrico Tassiremoved debug code
2008-12-16 Enrico Tassifixed a bug, it used to report o wrong is_normal bit...
2008-12-16 Enrico Tassimake it compile again
2008-12-16 Enrico Tassiwrap object_not_found
2008-12-16 Enrico Tassimove the printing in the right place
2008-12-16 Enrico Tassiauto expansion of \tex macros added as a switch in...
2008-12-16 Enrico Tassiadded one asser
2008-12-15 Enrico Tassidep.opt regenerated
2008-12-15 Enrico Tassiadded unification hints
2008-12-15 Wilmer RicciottiSome changes to the pullback test, for debugging
2008-12-15 Wilmer RicciottiFirst attempt to implement unification hints.
2008-12-15 Enrico Tassiuse named types to force some constraints asap
2008-12-15 Enrico TassiTo check if a term is type, do a whd of its sort before...
2008-12-15 Enrico Tassi...
2008-12-15 Enrico Tassiaded some whd, you should be able to declare something...
2008-12-14 Claudio Sacerdoti... The library is no longer automatically used during...
2008-12-14 Ferruccio Guidi- improved logging
2008-12-14 Ferruccio Guidinew kernel basic_ag (with absolute local references)
2008-12-14 Ferruccio Guidiwe are changing the kernel version from basic_rg to...
2008-12-14 Ferruccio GuidiautItem : the uris of the objects involved in the impli...
2008-12-14 Enrico Tassi...
2008-12-14 Enrico Tassieureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg...
2008-12-14 Enrico Tassi...
2008-12-12 Ferruccio Guidiimproved type hierarchy management
2008-12-12 Claudio Sacerdoti... ...
2008-12-12 Claudio Sacerdoti... A parser (and a scanner) to import "~C" files into...
2008-12-12 Claudio Sacerdoti... ...
2008-12-12 Claudio Sacerdoti... 1. new expressions AND, OR, XOR
2008-12-12 Ferruccio Guidi- basic_rg: architectural bug fix
2008-12-12 Enrico Tassi...
2008-12-12 Enrico Tassiadded some hardcoded universes, needed to typecheck...
2008-12-12 Enrico Tassiadded some messages
2008-12-12 Enrico Tassiadded empty_db, usefull to avoid translating all old...
2008-12-12 Enrico Tassiuse new function to clear caches so that objects are...
2008-12-12 Enrico Tassibetter error message, functions to clear various caches...
2008-12-12 Enrico Tassithanks to the new fixes to notation, I can define ...
2008-12-12 Enrico Tassipattern matching over Ast.Case simplified:
2008-12-11 Claudio Sacerdoti... Applications are now processed from left to right.
2008-12-11 Enrico Tassisupport for mathml mpadded tag added (allows to overlap...
2008-12-10 Ferruccio Guidi- new semantic log system
2008-12-09 Ferruccio Guidifirst version of kernel "basic_rg"
2008-12-09 Enrico Tassinew disambiguatio attached with the right universe...
next