| 2008-04-11 |
Enrico Tassi | Conversion of 2 lambdas was not requiring equality... |
commit | commitdiff | tree | snapshot |
| 2008-04-11 |
Enrico Tassi | context of types built in the reverse order |
commit | commitdiff | tree | snapshot |
| 2008-04-11 |
Enrico Tassi | added a simplify to prevent the generation of an ugly fix |
commit | commitdiff | tree | snapshot |
| 2008-04-11 |
Enrico Tassi | implemented inductive and less parentheses |
commit | commitdiff | tree | snapshot |
| 2008-04-10 |
Claudio Sacerdoti... | The cache of objects is now used also for cofixpoints. |
commit | commitdiff | tree | snapshot |
| 2008-04-10 |
Claudio Sacerdoti... | New: cache of translated fixpoints (to avoid the genera... |
commit | commitdiff | tree | snapshot |
| 2008-04-10 |
Claudio Sacerdoti... | does_not_occur exported to be used in oCic2NCic |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Claudio Sacerdoti... | Bug fixed: references to CoFix are CoFix, not Fix. |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | print unnamed variables as __n |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | switch off profilers |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | pp with parenthesis only when necessary and with some... |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Claudio Sacerdoti... | Fixed serious bug that occurred only in the following... |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | better pp in Appl |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | better pp |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | pretty printer on steroids |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Claudio Sacerdoti... | Added some "\n" here and there to the pretty-printing... |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Claudio Sacerdoti... | Grave bug fixed: Ce that point to definitions were... |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | added profiling on/off |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | invalidate fixed |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | allow to switch profiling on and off on the fly |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | removed two useless calls to the environment, one still... |
commit | commitdiff | tree | snapshot |
| 2008-04-09 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Variables are no longer experted (cooking is now implem... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Swapped arguments in error message. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Variables having a body can occur in cooked terms and... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Fix over the previous one: Var-LetIn abstractions shoul... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Error message improved. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Cooking w.r.t. variables with bodies is now implemented... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Fix name capture in cofix. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | To test the translation. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Name capture fixed. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Improved error messages in place of "sort elimination... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Seed reset before each convert_obj. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Use seed to avoid further name clashes. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Incredible, but true! Our name mangling clashed with... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Cooked objects are no longer well typed in the uncooked... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Improved eat_prods error message (at the cost of passin... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | The old kernel does not accept ens whose order is diffe... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Bad alpha-conversion by Enrico fixed. |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | Bug fixed: the ens need not be ordered w.r.t. the decla... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | j off by one in error message |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | fix_outty partially fixed: missing lifts in args and ens |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Claudio Sacerdoti... | fix_outty fixed in order to perform eta-expansion when... |
commit | commitdiff | tree | snapshot |
| 2008-04-08 |
Enrico Tassi | added simplify to avoid ugly proofterm |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Claudio Sacerdoti... | Tentative (and bad!) fix of outtypes in non-dependent... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Claudio Sacerdoti... | Cooking discriminated into cooking in types (using... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Claudio Sacerdoti... | Pretty-printing of definitions fixed. |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Claudio Sacerdoti... | Cooking implemented (not tested yet). |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Claudio Sacerdoti... | Reports improved. |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Claudio Sacerdoti... | Debugging code fixed. |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added invalidate to clear the cache and ease the compar... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | commented out uris of objs that do not compile properly |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added comparison with old kernel |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | fixed error message for eat prods |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | invalidate |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | uris relative to axioms are translated in the right way |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added invalidate |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added preliminary checks for indtys |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | call get_obj instead of get_cooked_obj ~trust:false |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added case of const and axiom |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added # to comment |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | better printings |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | the explicit type in a LetIn must be typecheckd before... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | opt compilation enabled, removed some pps, check has... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | lefts_ad_tys properly sorted, added some metasenv here... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | lefts_and_tys was tys@lefts, CSC claims it was working... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added a list of uris to ease debugging |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | print the excpetion and raise it again, seems to produc... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | new constants have depth = max_int insted of 0 so that... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | off by one in calling count_from |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | fixed bug in translating Fix, recno was not properly... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | added a pretty printing of the new object and use argv... |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | context, metasenv and subst made mandatory in CicPp |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | guarded by has a nice error message |
commit | commitdiff | tree | snapshot |
| 2008-04-07 |
Enrico Tassi | reference type made private, added mk_constructor to... |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | some debug printings |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | added to the cache a boolean to state if the object is |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | fix |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | today it seems that the substituted should be lifted... |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | added ppobj |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | type_of_constant was retunrning the type of the wrong... |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | fixed list.nth and added some paretheses |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | added some printings and catched more exceptions |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | removed useless printing |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | iterator map was mapping Lambdas to Prods!!! |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | debugging started |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | type of constant ported |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | added add_obj to store objects in the environment,... |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | logger added |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | added get_obj in nCicEnvironment that returns an object... |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | indentation fixed |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | returns_a_counductive implemented |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | type_of_branch ported and optimized to not lift the... |
commit | commitdiff | tree | snapshot |
| 2008-04-04 |
Enrico Tassi | is_really_smaller ported, still to understand the case... |
commit | commitdiff | tree | snapshot |
| 2008-04-03 |
Enrico Tassi | debujin implemented with the map recursor |
commit | commitdiff | tree | snapshot |
| 2008-04-03 |
Enrico Tassi | bug found rewriting the kernel backported: n instead... |
commit | commitdiff | tree | snapshot |
| 2008-04-03 |
Enrico Tassi | non debruijned constructor may be useless elswere,... |
commit | commitdiff | tree | snapshot |
| 2008-04-03 |
Enrico Tassi | guarded_by_destructor ported, many auxiliary functions... |
commit | commitdiff | tree | snapshot |
| next |
projects / helm.git / shortlog