2008-12-24 |
Enrico Tassi | added some virtuals |
commit | commitdiff | tree | snapshot |
2008-12-24 |
Enrico Tassi | bug fixed, all convertible was called without a metasenv |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Claudio Sacerdoti... | Just copied here from formal_topologies.ma. |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Claudio Sacerdoti... | More (ugly) work. |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Enrico Tassi | Beginning of o-basic_topologies. |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Enrico Tassi | Some clean up. |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Enrico Tassi | Concrete Spaces defined but... they require about 20m... |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Enrico Tassi | 1 more lemma |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Enrico Tassi | one line |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Enrico Tassi | some work |
commit | commitdiff | tree | snapshot |
2008-12-22 |
Claudio Sacerdoti... | ums got rid of |
commit | commitdiff | tree | snapshot |
2008-12-21 |
Claudio Sacerdoti... | 1) no more DAEMONS |
commit | commitdiff | tree | snapshot |
2008-12-21 |
Enrico Tassi | merged commits, the same proof is missing :-( |
commit | commitdiff | tree | snapshot |
2008-12-21 |
Enrico Tassi | bleah |
commit | commitdiff | tree | snapshot |
2008-12-21 |
Claudio Sacerdoti... | Using the new category SET. |
commit | commitdiff | tree | snapshot |
2008-12-21 |
Claudio Sacerdoti... | New category SET (whose objects are setoids). |
commit | commitdiff | tree | snapshot |
2008-12-20 |
Ferruccio Guidi | we started the support for naive sort inclusion |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | better pp of virtuals |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | more pps |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | type3 |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | ranking hopefully fixed |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | fix exponentiation |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | go notation go! |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | fixed, it seems the new handling of hints in some rare... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | added aliases for _ and fixed greek leters thanks to... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | better pps |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | handles bad Appl |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | added better debug_pps and add_user_provided_unificatio... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | added unification hint |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | unification hint |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | lambda case fixed, used to not properly use the expecte... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | added 'unification hint command to add a term to the... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | identity coercions are not really inserted, just used... |
commit | commitdiff | tree | snapshot |
2008-12-19 |
Enrico Tassi | .... |
commit | commitdiff | tree | snapshot |
2008-12-18 |
Claudio Sacerdoti... | Stupid bug fixed: checkin the type in place of the... |
commit | commitdiff | tree | snapshot |
2008-12-18 |
Claudio Sacerdoti... | New disambiguation commented out. |
commit | commitdiff | tree | snapshot |
2008-12-18 |
Claudio Sacerdoti... | Many axioms are now proved... using many more (but... |
commit | commitdiff | tree | snapshot |
2008-12-18 |
Claudio Sacerdoti... | Now it compiles again. |
commit | commitdiff | tree | snapshot |
2008-12-18 |
Claudio Sacerdoti... | Refinement of axioms fixed. We did not check that the... |
commit | commitdiff | tree | snapshot |
2008-12-18 |
Ferruccio Guidi | - improved logging |
commit | commitdiff | tree | snapshot |
2008-12-18 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-17 |
Ferruccio Guidi | we started the support for the coercions "alle" and... |
commit | commitdiff | tree | snapshot |
2008-12-17 |
Enrico Tassi | foo overlap |
commit | commitdiff | tree | snapshot |
2008-12-17 |
Enrico Tassi | foo overlap |
commit | commitdiff | tree | snapshot |
2008-12-17 |
Enrico Tassi | .... |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Ferruccio Guidi | we added the implicit coercion for modus tollens |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | previous change was causing divergence |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | hints work better now |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | hints attached |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | removed debug code |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | fixed a bug, it used to report o wrong is_normal bit... |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | make it compile again |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | wrap object_not_found |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | move the printing in the right place |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | auto expansion of \tex macros added as a switch in... |
commit | commitdiff | tree | snapshot |
2008-12-16 |
Enrico Tassi | added one asser |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Enrico Tassi | dep.opt regenerated |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Enrico Tassi | added unification hints |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Wilmer Ricciotti | Some changes to the pullback test, for debugging |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Wilmer Ricciotti | First attempt to implement unification hints. |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Enrico Tassi | use named types to force some constraints asap |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Enrico Tassi | To check if a term is type, do a whd of its sort before... |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-15 |
Enrico Tassi | aded some whd, you should be able to declare something... |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Claudio Sacerdoti... | The library is no longer automatically used during... |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Ferruccio Guidi | - improved logging |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Ferruccio Guidi | new kernel basic_ag (with absolute local references) |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Ferruccio Guidi | we are changing the kernel version from basic_rg to... |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Ferruccio Guidi | autItem : the uris of the objects involved in the impli... |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Enrico Tassi | eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg... |
commit | commitdiff | tree | snapshot |
2008-12-14 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Ferruccio Guidi | improved type hierarchy management |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Claudio Sacerdoti... | A parser (and a scanner) to import "~C" files into... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Claudio Sacerdoti... | 1. new expressions AND, OR, XOR |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Ferruccio Guidi | - basic_rg: architectural bug fix |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | added some hardcoded universes, needed to typecheck... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | added some messages |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | added empty_db, usefull to avoid translating all old... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | use new function to clear caches so that objects are... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | better error message, functions to clear various caches... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | thanks to the new fixes to notation, I can define ... |
commit | commitdiff | tree | snapshot |
2008-12-12 |
Enrico Tassi | pattern matching over Ast.Case simplified: |
commit | commitdiff | tree | snapshot |
2008-12-11 |
Claudio Sacerdoti... | Applications are now processed from left to right. |
commit | commitdiff | tree | snapshot |
2008-12-11 |
Enrico Tassi | support for mathml mpadded tag added (allows to overlap... |
commit | commitdiff | tree | snapshot |
2008-12-10 |
Ferruccio Guidi | - new semantic log system |
commit | commitdiff | tree | snapshot |
2008-12-09 |
Ferruccio Guidi | first version of kernel "basic_rg" |
commit | commitdiff | tree | snapshot |
2008-12-09 |
Enrico Tassi | new disambiguatio attached with the right universe... |
commit | commitdiff | tree | snapshot |
2008-12-09 |
Enrico Tassi | raise uncertain when a sort is not a sort but may be... |
commit | commitdiff | tree | snapshot |
2008-12-09 |
Enrico Tassi | better coercions indexing and lookup |
commit | commitdiff | tree | snapshot |
next |