| 2008-05-12 |
Claudio Sacerdoti... | trust is always false by default |
blob | commitdiff | raw |
| 2008-05-12 |
Claudio Sacerdoti... | trust implemented, but in the nCicTypeChecker! |
blob | commitdiff | raw | diff to current |
| 2008-05-12 |
Claudio Sacerdoti... | New implementation of CicEnvironment: |
blob | commitdiff | raw | diff to current |
| 2008-05-07 |
Claudio Sacerdoti... | Partially reverted bad merge by Enrico that re-introduc... |
blob | commitdiff | raw | diff to current |
| 2008-05-05 |
Enrico Tassi | get_check_fix and cofix unified, bug regarding debruijn... |
blob | commitdiff | raw | diff to current |
| 2008-05-05 |
Enrico Tassi | fix_left_in_constr still broken, ask enrico |
blob | commitdiff | raw | diff to current |
| 2008-05-05 |
Enrico Tassi | guarded_by_constructors implemented, some cleanup here... |
blob | commitdiff | raw | diff to current |
| 2008-04-30 |
Claudio Sacerdoti... | Implementation of guarded_by_destructor is now complete... |
blob | commitdiff | raw | diff to current |
| 2008-04-30 |
Claudio Sacerdoti... | stupid error fixed |
blob | commitdiff | raw | diff to current |
| 2008-04-30 |
Claudio Sacerdoti... | fixed_args fixed to accept passing a partially applied... |
blob | commitdiff | raw | diff to current |
| 2008-04-30 |
Enrico Tassi | added check on all bodies, only the one we actually... |
blob | commitdiff | raw | diff to current |
| 2008-04-30 |
Enrico Tassi | fixed wrong Rel, still to do: Fix(i,j) applied to dange... |
blob | commitdiff | raw | diff to current |
| 2008-04-30 |
Enrico Tassi | guarded_by_destructors on steroids |
blob | commitdiff | raw | diff to current |
| 2008-04-28 |
Claudio Sacerdoti... | Avoid (whd ~delta:true) during guarded_by_destructors... |
blob | commitdiff | raw | diff to current |
| 2008-04-23 |
Enrico Tassi | ported the instantiate-left-params-to-calculate-rec... |
blob | commitdiff | raw | diff to current |
| 2008-04-22 |
Enrico Tassi | added a call to ppcontext in the case of appl, to ease... |
blob | commitdiff | raw | diff to current |
| 2008-04-19 |
Enrico Tassi | better error message |
blob | commitdiff | raw | diff to current |
| 2008-04-18 |
Enrico Tassi | Appl case in is_really_smaller fixed as in the old... |
blob | commitdiff | raw | diff to current |
| 2008-04-17 |
Enrico Tassi | is_really_smaller in sync with old kernel, impossible... |
blob | commitdiff | raw | diff to current |
| 2008-04-15 |
Enrico Tassi | get_checked_fix -> get_checked_fixes |
blob | commitdiff | raw | diff to current |
| 2008-04-15 |
Enrico Tassi | do not use an implicit but a sort as a neutral term... |
blob | commitdiff | raw | diff to current |
| 2008-04-14 |
Enrico Tassi | better error message |
blob | commitdiff | raw | diff to current |
| 2008-04-14 |
Enrico Tassi | fixed positivity conditions |
blob | commitdiff | raw | diff to current |
| 2008-04-11 |
Enrico Tassi | quinck and untested implementation of positivity condit... |
blob | commitdiff | raw | diff to current |
| 2008-04-11 |
Enrico Tassi | context of types built in the reverse order |
blob | commitdiff | raw | diff to current |
| 2008-04-09 |
Enrico Tassi | removed two useless calls to the environment, one still... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Swapped arguments in error message. |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Error message improved. |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | To test the translation. |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Improved error messages in place of "sort elimination... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Improved eat_prods error message (at the cost of passin... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | j off by one in error message |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | fixed error message for eat prods |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | added preliminary checks for indtys |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | opt compilation enabled, removed some pps, check has... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | lefts_ad_tys properly sorted, added some metasenv here... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | off by one in calling count_from |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | context, metasenv and subst made mandatory in CicPp |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | guarded by has a nice error message |
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 | some debug printings |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | type_of_constant was retunrning the type of the wrong... |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | debugging started |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | type of constant ported |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | logger added |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | indentation fixed |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | returns_a_counductive implemented |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | type_of_branch ported and optimized to not lift the... |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | is_really_smaller ported, still to understand the case... |
blob | commitdiff | raw | diff to current |
| 2008-04-03 |
Enrico Tassi | debujin implemented with the map recursor |
blob | commitdiff | raw | diff to current |
| 2008-04-03 |
Enrico Tassi | non debruijned constructor may be useless elswere,... |
blob | commitdiff | raw | diff to current |
| 2008-04-03 |
Enrico Tassi | guarded_by_destructor ported, many auxiliary functions... |
blob | commitdiff | raw | diff to current |
| 2008-04-02 |
Enrico Tassi | added slim version of does_not_occur |
blob | commitdiff | raw | diff to current |
| 2008-04-01 |
Claudio Sacerdoti... | typeof_obj0 implemented |
blob | commitdiff | raw | diff to current |
| 2008-04-01 |
Claudio Sacerdoti... | 1) added get_checked_indtys that returns the whole... |
blob | commitdiff | raw | diff to current |
| 2008-03-31 |
Claudio Sacerdoti... | Large amount of duplicated code (still in comments... |
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-27 |
Enrico Tassi | more cases of the type checker honoured, still missing... |
blob | commitdiff | raw | diff to current |
| 2008-03-27 |
Enrico Tassi | added is_closed to nCicUtils. |
blob | commitdiff | raw | diff to current |
| 2008-03-27 |
Enrico Tassi | insert comments of old tpechecker |
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