]> matita.cs.unibo.it Git - helm.git/history - helm
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
more pps
[helm.git] / helm /
2008-12-19 Enrico Tassimore pps tree | commitdiff
2008-12-19 Enrico Tassitype3 tree | commitdiff
2008-12-19 Enrico Tassiranking hopefully fixed tree | commitdiff
2008-12-19 Enrico Tassi... tree | commitdiff
2008-12-19 Enrico Tassifix exponentiation tree | commitdiff
2008-12-19 Enrico Tassigo notation go! tree | commitdiff
2008-12-19 Enrico Tassifixed, it seems the new handling of hints in some rare... tree | commitdiff
2008-12-19 Enrico Tassi... tree | commitdiff
2008-12-19 Enrico Tassi... tree | commitdiff
2008-12-19 Enrico Tassi... tree | commitdiff
2008-12-19 Enrico Tassiadded aliases for _ and fixed greek leters thanks to... tree | commitdiff
2008-12-19 Enrico Tassibetter pps tree | commitdiff
2008-12-19 Enrico Tassihandles bad Appl tree | commitdiff
2008-12-19 Enrico Tassiadded better debug_pps and add_user_provided_unificatio... tree | commitdiff
2008-12-19 Enrico Tassi... tree | commitdiff
2008-12-19 Enrico Tassiadded unification hint tree | commitdiff
2008-12-19 Enrico Tassiunification hint tree | commitdiff
2008-12-19 Enrico Tassilambda case fixed, used to not properly use the expecte... tree | commitdiff
2008-12-19 Enrico Tassiadded 'unification hint command to add a term to the... tree | commitdiff
2008-12-19 Enrico Tassiidentity coercions are not really inserted, just used... tree | commitdiff
2008-12-19 Enrico Tassi.... tree | commitdiff
2008-12-18 Claudio Sacerdoti... Stupid bug fixed: checkin the type in place of the... tree | commitdiff
2008-12-18 Claudio Sacerdoti... New disambiguation commented out. tree | commitdiff
2008-12-18 Claudio Sacerdoti... Many axioms are now proved... using many more (but... tree | commitdiff
2008-12-18 Claudio Sacerdoti... Now it compiles again. tree | commitdiff
2008-12-18 Claudio Sacerdoti... Refinement of axioms fixed. We did not check that the... tree | commitdiff
2008-12-18 Ferruccio Guidi- improved logging tree | commitdiff
2008-12-18 Enrico Tassi... tree | commitdiff
2008-12-17 Ferruccio Guidiwe started the support for the coercions "alle" and... tree | commitdiff
2008-12-17 Enrico Tassifoo overlap tree | commitdiff
2008-12-17 Enrico Tassifoo overlap tree | commitdiff
2008-12-17 Enrico Tassi.... tree | commitdiff
2008-12-16 Ferruccio Guidiwe added the implicit coercion for modus tollens tree | commitdiff
2008-12-16 Enrico Tassiprevious change was causing divergence tree | commitdiff
2008-12-16 Enrico Tassihints work better now tree | commitdiff
2008-12-16 Enrico Tassihints attached tree | commitdiff
2008-12-16 Enrico Tassiremoved debug code tree | commitdiff
2008-12-16 Enrico Tassifixed a bug, it used to report o wrong is_normal bit... tree | commitdiff
2008-12-16 Enrico Tassimake it compile again tree | commitdiff
2008-12-16 Enrico Tassiwrap object_not_found tree | commitdiff
2008-12-16 Enrico Tassimove the printing in the right place tree | commitdiff
2008-12-16 Enrico Tassiauto expansion of \tex macros added as a switch in... tree | commitdiff
2008-12-16 Enrico Tassiadded one asser tree | commitdiff
2008-12-15 Enrico Tassidep.opt regenerated tree | commitdiff
2008-12-15 Enrico Tassiadded unification hints tree | commitdiff
2008-12-15 Wilmer RicciottiSome changes to the pullback test, for debugging tree | commitdiff
2008-12-15 Wilmer RicciottiFirst attempt to implement unification hints. tree | commitdiff
2008-12-15 Enrico Tassiuse named types to force some constraints asap tree | commitdiff
2008-12-15 Enrico TassiTo check if a term is type, do a whd of its sort before... tree | commitdiff
2008-12-15 Enrico Tassi... tree | commitdiff
2008-12-15 Enrico Tassiaded some whd, you should be able to declare something... tree | commitdiff
2008-12-14 Claudio Sacerdoti... The library is no longer automatically used during... tree | commitdiff
2008-12-14 Ferruccio Guidi- improved logging tree | commitdiff
2008-12-14 Ferruccio Guidinew kernel basic_ag (with absolute local references) tree | commitdiff
2008-12-14 Ferruccio Guidiwe are changing the kernel version from basic_rg to... tree | commitdiff
2008-12-14 Ferruccio GuidiautItem : the uris of the objects involved in the impli... tree | commitdiff
2008-12-14 Enrico Tassi... tree | commitdiff
2008-12-14 Enrico Tassieureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg... tree | commitdiff
2008-12-14 Enrico Tassi... tree | commitdiff
2008-12-12 Ferruccio Guidiimproved type hierarchy management tree | commitdiff
2008-12-12 Claudio Sacerdoti... ... tree | commitdiff
2008-12-12 Claudio Sacerdoti... A parser (and a scanner) to import "~C" files into... tree | commitdiff
2008-12-12 Claudio Sacerdoti... ... tree | commitdiff
2008-12-12 Claudio Sacerdoti... 1. new expressions AND, OR, XOR tree | commitdiff
2008-12-12 Ferruccio Guidi- basic_rg: architectural bug fix tree | commitdiff
2008-12-12 Enrico Tassi... tree | commitdiff
2008-12-12 Enrico Tassiadded some hardcoded universes, needed to typecheck... tree | commitdiff
2008-12-12 Enrico Tassiadded some messages tree | commitdiff
2008-12-12 Enrico Tassiadded empty_db, usefull to avoid translating all old... tree | commitdiff
2008-12-12 Enrico Tassiuse new function to clear caches so that objects are... tree | commitdiff
2008-12-12 Enrico Tassibetter error message, functions to clear various caches... tree | commitdiff
2008-12-12 Enrico Tassithanks to the new fixes to notation, I can define ... tree | commitdiff
2008-12-12 Enrico Tassipattern matching over Ast.Case simplified: tree | commitdiff
2008-12-11 Claudio Sacerdoti... Applications are now processed from left to right. tree | commitdiff
2008-12-11 Enrico Tassisupport for mathml mpadded tag added (allows to overlap... tree | commitdiff
2008-12-10 Ferruccio Guidi- new semantic log system tree | commitdiff
2008-12-09 Ferruccio Guidifirst version of kernel "basic_rg" tree | commitdiff
2008-12-09 Enrico Tassinew disambiguatio attached with the right universe... tree | commitdiff
2008-12-09 Enrico Tassiraise uncertain when a sort is not a sort but may be... tree | commitdiff
2008-12-09 Enrico Tassibetter coercions indexing and lookup tree | commitdiff
2008-12-09 Enrico Tassibetter max function (instead of @) for combining universes tree | commitdiff
2008-12-09 Enrico Tassiadded an exception tree | commitdiff
2008-12-09 Enrico Tassisaturate was not returning the correct (saturated)... tree | commitdiff
2008-12-09 Enrico Tassifixed notation tree | commitdiff
2008-12-09 Enrico Tassi... tree | commitdiff
2008-12-09 Enrico Tassioption to collapse all tex macros implemented tree | commitdiff
2008-12-08 Claudio Sacerdoti... A (boring and long) once-in-a-life exercise on proving... tree | commitdiff
2008-12-08 Enrico Tassinon active but almost working implementation of \TeX... tree | commitdiff
2008-12-08 Enrico Tassialt-l for not working nymore for \fox where x was in... tree | commitdiff
2008-12-08 Enrico Tassi... tree | commitdiff
2008-12-08 Enrico Tassibetter replacement for \\def tree | commitdiff
2008-12-08 Enrico Tassi3.5 -> 35 to help crappy latex tree | commitdiff
2008-12-07 Claudio Sacerdoti... New exception considered. tree | commitdiff
2008-12-07 Claudio Sacerdoti... Bug fixed: every time we form a Prod, we must typecheck... tree | commitdiff
2008-12-07 Enrico Tassibetter images tree | commitdiff
2008-12-06 Enrico Tassinew concept of virtuals, defined only in the gui that... tree | commitdiff
2008-12-06 Ferruccio GuidimetaAut: now we use hash tables properly (processing... tree | commitdiff
2008-12-05 Claudio Sacerdoti... new exception captured tree | commitdiff
2008-12-05 Claudio Sacerdoti... Added new syntax Type[n] where n is a number. tree | commitdiff
2008-12-05 Claudio Sacerdoti... Debugging code removed. tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.