| 2009-01-21 |
Enrico Tassi | a bit of work done while travelling to padova
|
commit | commitdiff | tree |
| 2009-01-19 |
Enrico Tassi | - new notation.ma file with local and common notation
|
commit | commitdiff | tree |
| 2009-01-19 |
Enrico Tassi | all pullbacks are attempted in sequence, removed many...
|
commit | commitdiff | tree |
| 2009-01-16 |
Enrico Tassi | ceommented out metasenv
|
commit | commitdiff | tree |
| 2009-01-16 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | the new coercion behaviour (variants + composition...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | added notation for 'Vdash
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | if the user attempts to insert a duplicate coercions...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | unvariant also for coercions to funclass
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | - name mangling changed, added __ to separate additional...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | no more universe inconsistency printed to stderr
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | coercions that are marked as variant are unfolded when...
|
commit | commitdiff | tree |
| 2009-01-15 |
Enrico Tassi | Coercions graph is printed between real types and not...
|
commit | commitdiff | tree |
| 2009-01-13 |
Enrico Tassi | many changes regarding coercions:
|
commit | commitdiff | tree |
| 2009-01-08 |
Enrico Tassi | more composites to make all happy!
|
commit | commitdiff | tree |
| 2009-01-08 |
Enrico Tassi | eq over SET1 and SET no longer used
|
commit | commitdiff | tree |
| 2009-01-08 |
Enrico Tassi | some more if/fi conversion due to the new . binding
|
commit | commitdiff | tree |
| 2009-01-08 |
Enrico Tassi | unary_morphism_N : seoidN -> setoidN -> setoidN (was...
|
commit | commitdiff | tree |
| 2009-01-08 |
Enrico Tassi | virtuals for () removed and bound to 'o'
|
commit | commitdiff | tree |
| 2009-01-06 |
Enrico Tassi | coercions reordering implemented
|
commit | commitdiff | tree |
| 2009-01-06 |
Enrico Tassi | updated
|
commit | commitdiff | tree |
| 2009-01-05 |
Enrico Tassi | removing (only from the interface) functions related...
|
commit | commitdiff | tree |
| 2009-01-05 |
Enrico Tassi | added help on virtuals and UTF-8 equivalence classes
|
commit | commitdiff | tree |
| 2009-01-05 |
Enrico Tassi | expand ligatures after \n too
|
commit | commitdiff | tree |
| 2009-01-05 |
Enrico Tassi | added := -> \def
|
commit | commitdiff | tree |
| 2009-01-05 |
Enrico Tassi | added some memory to virtuals eq classes
|
commit | commitdiff | tree |
| 2008-12-28 |
Enrico Tassi | removed duplicate notation
|
commit | commitdiff | tree |
| 2008-12-24 |
Enrico Tassi | added some virtuals
|
commit | commitdiff | tree |
| 2008-12-24 |
Enrico Tassi | bug fixed, all convertible was called without a metasenv
|
commit | commitdiff | tree |
| 2008-12-22 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-22 |
Enrico Tassi | Beginning of o-basic_topologies.
|
commit | commitdiff | tree |
| 2008-12-22 |
Enrico Tassi | Some clean up.
|
commit | commitdiff | tree |
| 2008-12-22 |
Enrico Tassi | Concrete Spaces defined but... they require about 20m...
|
commit | commitdiff | tree |
| 2008-12-22 |
Enrico Tassi | 1 more lemma
|
commit | commitdiff | tree |
| 2008-12-22 |
Enrico Tassi | one line
|
commit | commitdiff | tree |
| 2008-12-22 |
Enrico Tassi | some work
|
commit | commitdiff | tree |
| 2008-12-21 |
Enrico Tassi | merged commits, the same proof is missing :-(
|
commit | commitdiff | tree |
| 2008-12-21 |
Enrico Tassi | bleah
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | better pp of virtuals
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | more pps
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | type3
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ranking hopefully fixed
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | fix exponentiation
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | go notation go!
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | fixed, it seems the new handling of hints in some rare...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | added aliases for _ and fixed greek leters thanks to...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | better pps
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | handles bad Appl
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | added better debug_pps and add_user_provided_unification_hint
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | added unification hint
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | unification hint
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | lambda case fixed, used to not properly use the expected...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | added 'unification hint command to add a term to the...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | identity coercions are not really inserted, just used...
|
commit | commitdiff | tree |
| 2008-12-19 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2008-12-18 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-17 |
Enrico Tassi | foo overlap
|
commit | commitdiff | tree |
| 2008-12-17 |
Enrico Tassi | foo overlap
|
commit | commitdiff | tree |
| 2008-12-17 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | previous change was causing divergence
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | hints work better now
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | hints attached
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | removed debug code
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | fixed a bug, it used to report o wrong is_normal bit...
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | make it compile again
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | wrap object_not_found
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | move the printing in the right place
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | auto expansion of \tex macros added as a switch in...
|
commit | commitdiff | tree |
| 2008-12-16 |
Enrico Tassi | added one asser
|
commit | commitdiff | tree |
| 2008-12-15 |
Enrico Tassi | dep.opt regenerated
|
commit | commitdiff | tree |
| 2008-12-15 |
Enrico Tassi | added unification hints
|
commit | commitdiff | tree |
| 2008-12-15 |
Enrico Tassi | use named types to force some constraints asap
|
commit | commitdiff | tree |
| 2008-12-15 |
Enrico Tassi | To check if a term is type, do a whd of its sort before...
|
commit | commitdiff | tree |
| 2008-12-15 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-15 |
Enrico Tassi | aded some whd, you should be able to declare something...
|
commit | commitdiff | tree |
| 2008-12-14 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-14 |
Enrico Tassi | eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg...
|
commit | commitdiff | tree |
| 2008-12-14 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | added some hardcoded universes, needed to typecheck...
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | added some messages
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | added empty_db, usefull to avoid translating all old...
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | use new function to clear caches so that objects are...
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | better error message, functions to clear various caches...
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | thanks to the new fixes to notation, I can define ...
|
commit | commitdiff | tree |
| 2008-12-12 |
Enrico Tassi | pattern matching over Ast.Case simplified:
|
commit | commitdiff | tree |
| 2008-12-11 |
Enrico Tassi | support for mathml mpadded tag added (allows to overlap...
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | new disambiguatio attached with the right universe...
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | raise uncertain when a sort is not a sort but may be...
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | better coercions indexing and lookup
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | better max function (instead of @) for combining universes
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | added an exception
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | saturate was not returning the correct (saturated)...
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | fixed notation
|
commit | commitdiff | tree |
| next |
projects / helm.git / search