| 2008-12-15 |
Enrico Tassi | dep.opt regenerated |
tree | commitdiff |
| 2008-12-15 |
Enrico Tassi | added unification hints |
tree | commitdiff |
| 2008-12-15 |
Wilmer Ricciotti | Some changes to the pullback test, for debugging |
tree | commitdiff |
| 2008-12-15 |
Wilmer Ricciotti | First attempt to implement unification hints. |
tree | commitdiff |
| 2008-12-15 |
Enrico Tassi | use named types to force some constraints asap |
tree | commitdiff |
| 2008-12-15 |
Enrico Tassi | To 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 Tassi | aded 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 Guidi | new kernel basic_ag (with absolute local references) |
tree | commitdiff |
| 2008-12-14 |
Ferruccio Guidi | we are changing the kernel version from basic_rg to... |
tree | commitdiff |
| 2008-12-14 |
Ferruccio Guidi | autItem : the uris of the objects involved in the impli... |
tree | commitdiff |
| 2008-12-14 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-12-14 |
Enrico Tassi | eureka! match x with [ C gfds fsd fdg fdg fdg fd gfdg... |
tree | commitdiff |
| 2008-12-14 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-12-12 |
Ferruccio Guidi | improved 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 Tassi | added some hardcoded universes, needed to typecheck... |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | added some messages |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | added empty_db, usefull to avoid translating all old... |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | use new function to clear caches so that objects are... |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | better error message, functions to clear various caches... |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | thanks to the new fixes to notation, I can define ... |
tree | commitdiff |
| 2008-12-12 |
Enrico Tassi | pattern 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 Tassi | support 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 Guidi | first version of kernel "basic_rg" |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | new disambiguatio attached with the right universe... |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | raise uncertain when a sort is not a sort but may be... |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | better coercions indexing and lookup |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | better max function (instead of @) for combining universes |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | added an exception |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | saturate was not returning the correct (saturated)... |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | fixed notation |
tree | commitdiff |
| 2008-12-09 |
Enrico Tassi | option 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 Tassi | non active but almost working implementation of \TeX... |
tree | commitdiff |
| 2008-12-08 |
Enrico Tassi | alt-l for not working nymore for \fox where x was in... |
tree | commitdiff |
| 2008-12-08 |
Enrico Tassi | better replacement for \\def |
tree | commitdiff |
| 2008-12-08 |
Enrico Tassi | 3.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 Tassi | better images |
tree | commitdiff |
| 2008-12-06 |
Enrico Tassi | new concept of virtuals, defined only in the gui that... |
tree | commitdiff |
| 2008-12-06 |
Ferruccio Guidi | metaAut: 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 |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging code removed |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging instructions removed. |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Useless code removed. |
tree | commitdiff |
| 2008-12-05 |
Claudio Sacerdoti... | Case-sensitive fixes. |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | a few missing ~subst added to whd |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | coercions are there, but not heavily tested |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | if todo_dom was [] disambiguation was performed twice |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | still commented, but benchmarks the new/old disambiguti... |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | disambiguation takes ~mk_localization_tbl and not ... |
tree | commitdiff |
| 2008-12-05 |
Enrico Tassi | raise failure instead of uncertain if two terms are... |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | Fixes: |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | housekeeping: |
tree | commitdiff |
| 2008-12-04 |
Enrico Tassi | Bug fixed: pretty-printing of aliases when the OK butto... |
tree | commitdiff |
| 2008-12-03 |
Claudio Sacerdoti... | The aliases and multi_aliases in the lexicon status... |
tree | commitdiff |
| 2008-12-03 |
Ferruccio Guidi | improved interface for brgEnvironment |
tree | commitdiff |
| 2008-12-03 |
Ferruccio Guidi | log facility, initial environment for basic_rg |
tree | commitdiff |
| 2008-12-02 |
Ferruccio Guidi | - we updated some preambles to match that of nUri.ml |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | 0.5.6 almost ok |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | 0.5.6 |
tree | commitdiff |
| 2008-12-01 |
Ferruccio Guidi | we start a kernel for the version "basic with reverse... |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | all done |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | more ex and more notation |
tree | commitdiff |
| 2008-12-01 |
Enrico Tassi | better doc |
tree | commitdiff |
| 2008-12-01 |
Claudio Sacerdoti... | rt.op and check.opt removed from Makefile |
tree | commitdiff |
| 2008-11-30 |
Enrico Tassi | natural deduction support for lemmas with premises |
tree | commitdiff |
| 2008-11-30 |
Ferruccio Guidi | lambda-delta/toplevel: improved transformation from... |
tree | commitdiff |
| 2008-11-28 |
Ferruccio Guidi | cicDischarge: final fixup. Now correctly processes... |
tree | commitdiff |
| 2008-11-28 |
Ferruccio Guidi | ng_disambiguation ng_kernel ng_refiner disambiguation... |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | it works! |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | new disambiguator almost attached |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | \forall x:?. and \forall x. both generate a meta for... |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | metas for terms have height 3 |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | virtualbox guide almost ok |
tree | commitdiff |
| 2008-11-28 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-11-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-11-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-11-27 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | New modules stack: |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | cic_disambiguation splitted into disambiguation and... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | disambiguate.ml splitted into disambiguate.ml and cicDi... |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | 1. grafiteDisambiguator => multiPassDisambiguator |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | new kernel is compiled since the META of grafite_parser... |
tree | commitdiff |
| next |
projects / helm.git / history