| 2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
blob | commitdiff | raw |
| 2009-06-05 |
Claudio Sacerdoti... | The kernel _must_ check the correctness of the height... |
blob | commitdiff | raw | diff to current |
| 2009-06-03 |
Claudio Sacerdoti... | Huge commit with several changes: |
blob | commitdiff | raw | diff to current |
| 2009-05-15 |
Claudio Sacerdoti... | Patch to add a debugging string to HExtlib.split_nth... |
blob | commitdiff | raw | diff to current |
| 2009-05-14 |
Ferruccio Guidi | - hExtlib: added debugging information for split_nth |
blob | commitdiff | raw | diff to current |
| 2009-05-08 |
Claudio Sacerdoti... | The relevance list can be shorter than leftno (when... |
blob | commitdiff | raw | diff to current |
| 2009-05-05 |
Enrico Tassi | - pretty printer made robust in face of list_nth |
blob | commitdiff | raw | diff to current |
| 2009-04-29 |
Claudio Sacerdoti... | Refinement of inductive type implemented. |
blob | commitdiff | raw | diff to current |
| 2009-04-25 |
Claudio Sacerdoti... | Better error message. |
blob | commitdiff | raw | diff to current |
| 2009-04-06 |
Enrico Tassi | better error message |
blob | commitdiff | raw | diff to current |
| 2008-12-12 |
Enrico Tassi | better error message, functions to clear various caches... |
blob | commitdiff | raw | diff to current |
| 2008-12-09 |
Enrico Tassi | better max function (instead of @) for combining universes |
blob | commitdiff | raw | diff to current |
| 2008-12-05 |
Enrico Tassi | a few missing ~subst added to whd |
blob | commitdiff | raw | diff to current |
| 2008-10-27 |
Enrico Tassi | metasenv passed to get_relevance, Metas that stand... |
blob | commitdiff | raw | diff to current |
| 2008-10-14 |
Enrico Tassi | term refinement almost done, some functions exported... |
blob | commitdiff | raw | diff to current |
| 2008-10-13 |
Enrico Tassi | initial refiner .... |
blob | commitdiff | raw | diff to current |
| 2008-10-03 |
Enrico Tassi | - NCicPp.ppterm applies the substitution |
blob | commitdiff | raw | diff to current |
| 2008-08-01 |
Enrico Tassi | fixed recursiveness check |
blob | commitdiff | raw | diff to current |
| 2008-07-30 |
Enrico Tassi | fixed allowed sort elim |
blob | commitdiff | raw | diff to current |
| 2008-07-30 |
Claudio Sacerdoti... | Missing check in positivity implemented: we did not... |
blob | commitdiff | raw | diff to current |
| 2008-07-25 |
Enrico Tassi | - too strict check on left parameters of constructors... |
blob | commitdiff | raw | diff to current |
| 2008-07-23 |
Enrico Tassi | positivity check fixed |
blob | commitdiff | raw | diff to current |
| 2008-06-13 |
Wilmer Ricciotti | final relevance check |
blob | commitdiff | raw | diff to current |
| 2008-06-10 |
Wilmer Ricciotti | Added check of relevance lists for inductive types... |
blob | commitdiff | raw | diff to current |
| 2008-06-09 |
Wilmer Ricciotti | more proof irrelevance |
blob | commitdiff | raw | diff to current |
| 2008-06-04 |
Wilmer Ricciotti | Proof-irrelevance check for all applications (first... |
blob | commitdiff | raw | diff to current |
| 2008-06-04 |
Wilmer Ricciotti | incomplete irrelevance test commented out |
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 | relevance check partially implemented but bugged since... |
blob | commitdiff | raw | diff to current |
| 2008-05-29 |
Enrico Tassi | unused variables removed |
blob | commitdiff | raw | diff to current |
| 2008-05-29 |
Enrico Tassi | ref sync check fixed controlling fix/cofix coherence |
blob | commitdiff | raw | diff to current |
| 2008-05-19 |
Claudio Sacerdoti... | Here is where we should add relevance checks. |
blob | commitdiff | raw | diff to current |
| 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 |
| next |
projects / helm.git / history