| 2009-05-15 |
Claudio Sacerdoti... | Patch to add a debugging string to HExtlib.split_nth... |
blob | commitdiff | raw |
| 2009-05-14 |
Ferruccio Guidi | - hExtlib: added debugging information for split_nth |
blob | commitdiff | raw | diff to current |
| 2008-12-12 |
Enrico Tassi | better error message, functions to clear various caches... |
blob | commitdiff | raw |
| 2008-10-01 |
Enrico Tassi | commented out unfinished code |
blob | commitdiff | raw | diff to current |
| 2008-09-30 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2008-06-09 |
Wilmer Ricciotti | more proof irrelevance |
blob | commitdiff | raw | diff to current |
| 2008-05-30 |
Enrico Tassi | irrelevance check half implemented but already impossib... |
blob | commitdiff | raw | diff to current |
| 2008-05-29 |
Enrico Tassi | unused variables removed |
blob | commitdiff | raw | diff to current |
| 2008-05-19 |
Claudio Sacerdoti... | Bug fixed in computation of leftnos: variables were... |
blob | commitdiff | raw | diff to current |
| 2008-05-19 |
Claudio Sacerdoti... | CProp dropped in favour of a cprop universe exported... |
blob | commitdiff | raw | diff to current |
| 2008-05-19 |
Enrico Tassi | added leftno to references f inductive types and constr... |
blob | commitdiff | raw | diff to current |
| 2008-05-17 |
Claudio Sacerdoti... | Missing whd. |
blob | commitdiff | raw | diff to current |
| 2008-05-16 |
Enrico Tassi | added new implementation of universes |
blob | commitdiff | raw | diff to current |
| 2008-05-15 |
Enrico Tassi | (Approximated) inference of relevance implemented:... |
blob | commitdiff | raw | diff to current |
| 2008-05-15 |
Enrico Tassi | Bug fixed in computation of heights: a constant must... |
blob | commitdiff | raw | diff to current |
| 2008-05-15 |
Enrico Tassi | Implementation of calculation of heights. |
blob | commitdiff | raw | diff to current |
| 2008-05-15 |
Enrico Tassi | height of constants properly handled |
blob | commitdiff | raw | diff to current |
| 2008-05-14 |
Claudio Sacerdoti... | nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_... |
blob | commitdiff | raw | diff to current |
| 2008-05-14 |
Claudio Sacerdoti... | New licence used uniformly everywhere. |
blob | commitdiff | raw | diff to current |
| 2008-05-13 |
Claudio Sacerdoti... | Added boolean "is_inductive" to NReference.Ind |
blob | commitdiff | raw | diff to current |
| 2008-05-05 |
Enrico Tassi | CoFix cache implemented |
blob | commitdiff | raw | diff to current |
| 2008-05-01 |
Claudio Sacerdoti... | Last (???) bug about variables with bodies fixed: we... |
blob | commitdiff | raw | diff to current |
| 2008-05-01 |
Claudio Sacerdoti... | Another case where the presence of variables with bodie... |
blob | commitdiff | raw | diff to current |
| 2008-05-01 |
Claudio Sacerdoti... | Bug fixed: application without arguments generated... |
blob | commitdiff | raw | diff to current |
| 2008-04-24 |
Claudio Sacerdoti... | When going under a binder, a term must be converted... |
blob | commitdiff | raw | diff to current |
| 2008-04-22 |
Enrico Tassi | more strict check by CSC, I miss it |
blob | commitdiff | raw | diff to current |
| 2008-04-22 |
Enrico Tassi | fix cache comparison relaxed to URI and not REFERENCE |
blob | commitdiff | raw | diff to current |
| 2008-04-19 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2008-04-18 |
Enrico Tassi | workaround for some Set/Type problems |
blob | commitdiff | raw | diff to current |
| 2008-04-14 |
Enrico Tassi | leftno should be increased of the expnamedsubst, but... |
blob | commitdiff | raw | diff to current |
| 2008-04-14 |
Enrico Tassi | same_obj made more precise, fixed the order of the... |
blob | commitdiff | raw | diff to current |
| 2008-04-14 |
Enrico Tassi | ficed fixpoint cache usage for mutual fix |
blob | commitdiff | raw | diff to current |
| 2008-04-11 |
Enrico Tassi | use universe rank instead of Type0 |
blob | commitdiff | raw | diff to current |
| 2008-04-10 |
Claudio Sacerdoti... | The cache of objects is now used also for cofixpoints. |
blob | commitdiff | raw | diff to current |
| 2008-04-10 |
Claudio Sacerdoti... | New: cache of translated fixpoints (to avoid the genera... |
blob | commitdiff | raw | diff to current |
| 2008-04-09 |
Claudio Sacerdoti... | Fixed serious bug that occurred only in the following... |
blob | commitdiff | raw | diff to current |
| 2008-04-09 |
Claudio Sacerdoti... | Grave bug fixed: Ce that point to definitions were... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Variables having a body can occur in cooked terms and... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Fix over the previous one: Var-LetIn abstractions shoul... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Cooking w.r.t. variables with bodies is now implemented... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Fix name capture in cofix. |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Name capture fixed. |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Seed reset before each convert_obj. |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Use seed to avoid further name clashes. |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Incredible, but true! Our name mangling clashed with... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Cooked objects are no longer well typed in the uncooked... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | The old kernel does not accept ens whose order is diffe... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Bug fixed: the ens need not be ordered w.r.t. the decla... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | fix_outty partially fixed: missing lifts in args and ens |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | fix_outty fixed in order to perform eta-expansion when... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Claudio Sacerdoti... | Tentative (and bad!) fix of outtypes in non-dependent... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Claudio Sacerdoti... | Cooking discriminated into cooking in types (using... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Claudio Sacerdoti... | Cooking implemented (not tested yet). |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | uris relative to axioms are translated in the right way |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | new constants have depth = max_int insted of 0 so that... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | fixed bug in translating Fix, recno was not properly... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | reference type made private, added mk_constructor to... |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | debugging started |
blob | commitdiff | raw | diff to current |
| 2008-04-02 |
Enrico Tassi | added translation of Set to Type0 (avoid warning) |
blob | commitdiff | raw | diff to current |
| 2008-03-31 |
Claudio Sacerdoti... | 1) Impredicative sort "Set" removed everywhere. |
blob | commitdiff | raw | diff to current |
| 2008-03-25 |
Enrico Tassi | context for fixpoint body created in the hopefully... |
blob | commitdiff | raw | diff to current |
| 2008-03-25 |
Enrico Tassi | ported to the Cic LetIn with explicit type |
blob | commitdiff | raw | diff to current |
| 2008-02-21 |
Claudio Sacerdoti... | Avoid application to 0 arguments. |
blob | commitdiff | raw | diff to current |
| 2008-02-20 |
Enrico Tassi | splat_args is now better understood and debugged: we... |
blob | commitdiff | raw | diff to current |
| 2008-02-20 |
Enrico Tassi | added small test, fixed some bugs |
blob | commitdiff | raw | diff to current |
| 2008-02-20 |
Enrico Tassi | many fixed in translation functions |
blob | commitdiff | raw | diff to current |
| 2008-02-19 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2008-02-19 |
Enrico Tassi | snapshot inverse tranformation |
blob | commitdiff | raw | diff to current |
| 2008-02-19 |
Enrico Tassi | transformation almost finisced, not tested |
blob | commitdiff | raw | diff to current |
| 2008-02-13 |
Enrico Tassi | conversion half inplemented |
blob | commitdiff | raw | diff to current |
| 2008-01-30 |
Enrico Tassi | stub functions to make all compile |
blob | commitdiff | raw | diff to current |
|
projects / helm.git / history