2008-05-19 |
Claudio Sacerdoti... | Here is where we should add relevance checks. |
blob | commitdiff | raw |
2008-05-19 |
Claudio Sacerdoti... | Code simplification. |
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-18 |
Claudio Sacerdoti... | Bug fixed: when computing the left arguments, I was... |
blob | commitdiff | raw | diff to current |
2008-05-18 |
Claudio Sacerdoti... | New missing check implemented: the left parameters... |
blob | commitdiff | raw | diff to current |
2008-05-18 |
Claudio Sacerdoti... | Serious bug fixed: the max of two universes was compute... |
blob | commitdiff | raw | diff to current |
2008-05-18 |
Claudio Sacerdoti... | Error message improved. |
blob | commitdiff | raw | diff to current |
2008-05-17 |
Claudio Sacerdoti... | New check implemented: the sort of each constructor... |
blob | commitdiff | raw | diff to current |
2008-05-16 |
Enrico Tassi | added new implementation of universes |
blob | commitdiff | raw | diff to current |
2008-05-16 |
Enrico Tassi | used ind/coind information in references |
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... | list_iter2_default_value moved to HExtlib. 1 euro to... |
blob | commitdiff | raw | diff to current |
2008-05-14 |
Claudio Sacerdoti... | eat_lambdas and eat_or_subst_lambdas taken out of the... |
blob | commitdiff | raw | diff to current |
2008-05-14 |
Claudio Sacerdoti... | debruijn simplified. It could go in nCicUtils, but... |
blob | commitdiff | raw | diff to current |
2008-05-14 |
Claudio Sacerdoti... | Bug fixed: types were check for conversion in the wrong... |
blob | commitdiff | raw | diff to current |
2008-05-14 |
Claudio Sacerdoti... | We forgot an important check: the declared and expected... |
blob | commitdiff | raw | diff to current |
2008-05-14 |
Claudio Sacerdoti... | New checks for well-formedness of metasenvs and substs. |
blob | commitdiff | raw | diff to current |
2008-05-14 |
Claudio Sacerdoti... | map_hash moved to HExtlib |
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... | One more bug fixed: we tried to perform List.nth on... |
blob | commitdiff | raw | diff to current |
2008-05-13 |
Claudio Sacerdoti... | - is_closed removed from the kernel (it used to make... |
blob | commitdiff | raw | diff to current |
2008-05-13 |
Claudio Sacerdoti... | Type of conjecture and subst_entry made uniform. |
blob | commitdiff | raw | diff to current |
2008-05-13 |
Enrico Tassi | convertibility was taking a metasenv but not using it |
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-12 |
Claudio Sacerdoti... | trust is always false by default |
blob | commitdiff | raw | diff to current |
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 |
|