| 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 |
| 2008-12-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-09 |
Enrico Tassi | option to collapse all tex macros implemented
|
commit | commitdiff | tree |
| 2008-12-08 |
Enrico Tassi | non active but almost working implementation of \TeX...
|
commit | commitdiff | tree |
| 2008-12-08 |
Enrico Tassi | alt-l for not working nymore for \fox where x was in...
|
commit | commitdiff | tree |
| 2008-12-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-08 |
Enrico Tassi | better replacement for \\def
|
commit | commitdiff | tree |
| 2008-12-08 |
Enrico Tassi | 3.5 -> 35 to help crappy latex
|
commit | commitdiff | tree |
| 2008-12-07 |
Enrico Tassi | better images
|
commit | commitdiff | tree |
| 2008-12-06 |
Enrico Tassi | new concept of virtuals, defined only in the gui that...
|
commit | commitdiff | tree |
| 2008-12-05 |
Enrico Tassi | a few missing ~subst added to whd
|
commit | commitdiff | tree |
| 2008-12-05 |
Enrico Tassi | coercions are there, but not heavily tested
|
commit | commitdiff | tree |
| 2008-12-05 |
Enrico Tassi | if todo_dom was [] disambiguation was performed twice
|
commit | commitdiff | tree |
| 2008-12-05 |
Enrico Tassi | still commented, but benchmarks the new/old disambigution...
|
commit | commitdiff | tree |
| 2008-12-05 |
Enrico Tassi | disambiguation takes ~mk_localization_tbl and not ...
|
commit | commitdiff | tree |
| 2008-12-05 |
Enrico Tassi | raise failure instead of uncertain if two terms are...
|
commit | commitdiff | tree |
| 2008-12-04 |
Enrico Tassi | Fixes:
|
commit | commitdiff | tree |
| 2008-12-04 |
Enrico Tassi | housekeeping:
|
commit | commitdiff | tree |
| 2008-12-04 |
Enrico Tassi | Bug fixed: pretty-printing of aliases when the OK button...
|
commit | commitdiff | tree |
| 2008-12-02 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-12-01 |
Enrico Tassi | 0.5.6 almost ok
|
commit | commitdiff | tree |
| 2008-12-01 |
Enrico Tassi | 0.5.6
|
commit | commitdiff | tree |
| 2008-12-01 |
Enrico Tassi | all done
|
commit | commitdiff | tree |
| 2008-12-01 |
Enrico Tassi | more ex and more notation
|
commit | commitdiff | tree |
| 2008-12-01 |
Enrico Tassi | better doc
|
commit | commitdiff | tree |
| 2008-11-30 |
Enrico Tassi | natural deduction support for lemmas with premises
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | it works!
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | new disambiguator almost attached
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | \forall x:?. and \forall x. both generate a meta for...
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | metas for terms have height 3
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | virtualbox guide almost ok
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | New modules stack:
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | cic_disambiguation splitted into disambiguation and...
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | disambiguate.ml splitted into disambiguate.ml and cicDisambi...
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | 1. grafiteDisambiguator => multiPassDisambiguator
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | new kernel is compiled since the META of grafite_parser...
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | notation now digests Cic.Cast, not sure the precedence...
|
commit | commitdiff | tree |
| 2008-11-27 |
Enrico Tassi | disambiguation should not fail if the new refiner fails
|
commit | commitdiff | tree |
| 2008-11-26 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-26 |
Enrico Tassi | Re-added exception, just for now (debugging).
|
commit | commitdiff | tree |
| 2008-11-26 |
Enrico Tassi | almost done
|
commit | commitdiff | tree |
| 2008-11-26 |
Enrico Tassi | disambiguation even more abstracted
|
commit | commitdiff | tree |
| 2008-11-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-11-25 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search