| 2008-05-13 |
Claudio Sacerdoti... | Never commit before trying to compile... stupid typo... |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Used old kernel exception in place of brand new one. |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | - is_closed removed from the kernel (it used to make... |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Library factorized out. |
tree | commitdiff |
| 2008-05-13 |
Enrico Tassi | wrong test equality only fixed |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Type of conjecture and subst_entry made uniform. |
tree | commitdiff |
| 2008-05-13 |
Enrico Tassi | convertibility was taking a metasenv but not using it |
tree | commitdiff |
| 2008-05-13 |
Claudio Sacerdoti... | Added boolean "is_inductive" to NReference.Ind |
tree | commitdiff |
| 2008-05-12 |
Claudio Sacerdoti... | trust is always false by default |
tree | commitdiff |
| 2008-05-12 |
Claudio Sacerdoti... | trust implemented, but in the nCicTypeChecker! |
tree | commitdiff |
| 2008-05-12 |
Claudio Sacerdoti... | New implementation of CicEnvironment: |
tree | commitdiff |
| 2008-05-12 |
Enrico Tassi | height is stored in the reference, no need to fetch... |
tree | commitdiff |
| 2008-05-07 |
Claudio Sacerdoti... | Update after some more bug fixing. |
tree | commitdiff |
| 2008-05-07 |
Claudio Sacerdoti... | Partially reverted bad merge by Enrico that re-introduc... |
tree | commitdiff |
| 2008-05-05 |
Claudio Sacerdoti... | More bugs fixed. |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | get_check_fix and cofix unified, bug regarding debruijn... |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | get_checked_indtys can take a constructor reference |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | added mk_cofix |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | let corec |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | CoFix cache implemented |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | fix_left_in_constr still broken, ask enrico |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | guarded_by_constructors implemented, some cleanup here... |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | removed dead code |
tree | commitdiff |
| 2008-05-05 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-05-03 |
Claudio Sacerdoti... | Bug fixed in handling of explicit named substitutions... |
tree | commitdiff |
| 2008-05-03 |
Claudio Sacerdoti... | Broken XML files either fixed or removed. |
tree | commitdiff |
| 2008-05-01 |
Claudio Sacerdoti... | More precise classification of failures. |
tree | commitdiff |
| 2008-05-01 |
Claudio Sacerdoti... | List of all URIS comprising: |
tree | commitdiff |
| 2008-05-01 |
Claudio Sacerdoti... | More options can now be set at the beginning of the... |
tree | commitdiff |
| 2008-05-01 |
Claudio Sacerdoti... | Last (???) bug about variables with bodies fixed: we... |
tree | commitdiff |
| 2008-05-01 |
Claudio Sacerdoti... | Another case where the presence of variables with bodie... |
tree | commitdiff |
| 2008-05-01 |
Claudio Sacerdoti... | Bug fixed: application without arguments generated... |
tree | commitdiff |
| 2008-05-01 |
Claudio Sacerdoti... | New bug found. |
tree | commitdiff |
| 2008-04-30 |
Claudio Sacerdoti... | Things are getting better. |
tree | commitdiff |
| 2008-04-30 |
Claudio Sacerdoti... | Implementation of guarded_by_destructor is now complete... |
tree | commitdiff |
| 2008-04-30 |
Claudio Sacerdoti... | Reducing an open term should not be an error (or should... |
tree | commitdiff |
| 2008-04-30 |
Claudio Sacerdoti... | stupid error fixed |
tree | commitdiff |
| 2008-04-30 |
Claudio Sacerdoti... | fixed_args fixed to accept passing a partially applied... |
tree | commitdiff |
| 2008-04-30 |
Enrico Tassi | added check on all bodies, only the one we actually... |
tree | commitdiff |
| 2008-04-30 |
Enrico Tassi | fixed wrong Rel, still to do: Fix(i,j) applied to dange... |
tree | commitdiff |
| 2008-04-30 |
Enrico Tassi | guarded_by_destructors on steroids |
tree | commitdiff |
| 2008-04-29 |
Claudio Sacerdoti... | Tests status update. |
tree | commitdiff |
| 2008-04-28 |
Claudio Sacerdoti... | Avoid (whd ~delta:true) during guarded_by_destructors... |
tree | commitdiff |
| 2008-04-24 |
Claudio Sacerdoti... | Update... |
tree | commitdiff |
| 2008-04-24 |
Claudio Sacerdoti... | No more bugs on guarded_by_constructors in the old... |
tree | commitdiff |
| 2008-04-24 |
Claudio Sacerdoti... | When going under a binder, a term must be converted... |
tree | commitdiff |
| 2008-04-24 |
Claudio Sacerdoti... | Working and broken URIs. |
tree | commitdiff |
| 2008-04-23 |
Enrico Tassi | ported the instantiate-left-params-to-calculate-rec... |
tree | commitdiff |
| 2008-04-22 |
Enrico Tassi | more strict check by CSC, I miss it |
tree | commitdiff |
| 2008-04-22 |
Enrico Tassi | fix cache comparison relaxed to URI and not REFERENCE |
tree | commitdiff |
| 2008-04-22 |
Enrico Tassi | added a call to ppcontext in the case of appl, to ease... |
tree | commitdiff |
| 2008-04-22 |
Enrico Tassi | added ppcontext |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | better error message |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | impredicative set work around |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | impredicative set work around |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | associativity of -> fixed |
tree | commitdiff |
| 2008-04-19 |
Claudio Sacerdoti... | Added to flags to activate/disactivate pretty-printing... |
tree | commitdiff |
| 2008-04-19 |
Claudio Sacerdoti... | Uris must be stripped of their xpointers. |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | workaround for Pi associativity |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | workaround for some Set/Type problems |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | graph generation phase fixed |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | Appl case in is_really_smaller fixed as in the old... |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | is_really_smaller in sync with old kernel, impossible... |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | get_checked_fix -> get_checked_fixes |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | added comment |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | do not use an implicit but a sort as a neutral term... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | objects are typechecked to ensure there is a graph... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | leftno should be increased of the expnamedsubst, but... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | better error message |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | same_obj made more precise, fixed the order of the... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | ficed fixpoint cache usage for mutual fix |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | fixed positivity conditions |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | added mk_fix i j r that given an r of a fix generated... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | quinck and untested implementation of positivity condit... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | load the graph of objects that depend on the ones reque... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | use universe rank instead of Type0 |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | Type related failures fixed |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | better pp of objects |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | removed useless file |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | context of types built in the reverse order |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | implemented inductive and less parentheses |
tree | commitdiff |
| 2008-04-10 |
Claudio Sacerdoti... | The cache of objects is now used also for cofixpoints. |
tree | commitdiff |
| 2008-04-10 |
Claudio Sacerdoti... | New: cache of translated fixpoints (to avoid the genera... |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Bug fixed: references to CoFix are CoFix, not Fix. |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | print unnamed variables as __n |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | pp with parenthesis only when necessary and with some... |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Fixed serious bug that occurred only in the following... |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | better pp in Appl |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | better pp |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | pretty printer on steroids |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Added some "\n" here and there to the pretty-printing... |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Grave bug fixed: Ce that point to definitions were... |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | added profiling on/off |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | removed two useless calls to the environment, one still... |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Variables are no longer experted (cooking is now implem... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Swapped arguments in error message. |
tree | commitdiff |
| next |
projects / helm.git / history