| 2009-10-22 |
Enrico Tassi | new instantiate, only known bug is w.r.t. in/out scope... |
blob | commitdiff | raw |
| 2009-10-14 |
Claudio Sacerdoti... | Error message fixed (dereferencing must be done eagerly... |
blob | commitdiff | raw | diff to current |
| 2009-10-14 |
Claudio Sacerdoti... | Serious bug fixed: fix_sorts used to allow inference... |
blob | commitdiff | raw | diff to current |
| 2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
blob | commitdiff | raw | diff to current |
| 2009-07-20 |
Claudio Sacerdoti... | 1) The NG kernel now accepts only usage of declared... |
blob | commitdiff | raw | diff to current |
| 2009-07-17 |
Claudio Sacerdoti... | 1) added a function to retrieve all the universes curre... |
blob | commitdiff | raw | diff to current |
| 2009-06-23 |
Enrico Tassi | undo/serialization for universes implemented |
blob | commitdiff | raw | diff to current |
| 2009-06-23 |
Claudio Sacerdoti... | Debugging prerr_endlines removed. |
blob | commitdiff | raw | diff to current |
| 2009-06-23 |
Claudio Sacerdoti... | 1) NCicTypechecker.typecheck_obj removed, since it... |
blob | commitdiff | raw | diff to current |
| 2009-06-16 |
Claudio Sacerdoti... | 1) NCicLibrary (which is untrusted) moved after NCicUnt... |
blob | commitdiff | raw | diff to current |
| 2009-05-18 |
Enrico Tassi | removed useless function |
blob | commitdiff | raw | diff to current |
| 2009-05-18 |
Enrico Tassi | in the new kernel you can type Type[i] to mean Type_i... |
blob | commitdiff | raw | diff to current |
| 2008-12-19 |
Enrico Tassi | better pps |
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-10-20 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
blob | commitdiff | raw | diff to current |
| 2008-05-29 |
Enrico Tassi | unused variables removed |
blob | commitdiff | raw | diff to current |
| 2008-05-19 |
Claudio Sacerdoti... | We do not need to give cprop a special status yet. |
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-19 |
Enrico Tassi | renamed add_le_constraint to add_constraint since it... |
blob | commitdiff | raw | diff to current |
| 2008-05-18 |
Claudio Sacerdoti... | More effective optimization: avoid introducing already... |
blob | commitdiff | raw | diff to current |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed: since circular <= graphs are allowed, added... |
blob | commitdiff | raw | diff to current |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed and further code semplification in management... |
blob | commitdiff | raw | diff to current |
| 2008-05-17 |
Claudio Sacerdoti... | The code for universes was not correct in many borderli... |
blob | commitdiff | raw | diff to current |
| 2008-05-16 |
Enrico Tassi | added new implementation of universes |
blob | commitdiff | raw | diff to current |
| 2008-05-15 |
Enrico Tassi | New function get_relevance and new (not exported) funct... |
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 |
Enrico Tassi | fixed error message |
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... | Added boolean "is_inductive" to NReference.Ind |
blob | commitdiff | raw | diff to current |
| 2008-05-12 |
Claudio Sacerdoti... | New implementation of CicEnvironment: |
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 | get_checked_indtys can take a constructor reference |
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-11 |
Enrico Tassi | load the graph of objects that depend on the ones reque... |
blob | commitdiff | raw | diff to current |
| 2008-04-09 |
Claudio Sacerdoti... | Bug fixed: references to CoFix are CoFix, not Fix. |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | added invalidate |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | call get_obj instead of get_cooked_obj ~trust:false |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | added to the cache a boolean to state if the object is |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | removed useless printing |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | debugging started |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | added add_obj to store objects in the environment,... |
blob | commitdiff | raw | diff to current |
| 2008-04-04 |
Enrico Tassi | added get_obj in nCicEnvironment that returns an object... |
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-02-20 |
Enrico Tassi | added small test, fixed some bugs |
blob | commitdiff | raw | diff to current |
| 2008-02-19 |
Enrico Tassi | transformation almost finisced, not tested |
blob | commitdiff | raw | diff to current |
| 2008-02-18 |
Enrico Tassi | some bits of reduction, reusing psubst |
blob | commitdiff | raw | diff to current |
| 2008-02-13 |
Enrico Tassi | conversion half inplemented |
blob | commitdiff | raw | diff to current |
| 2008-02-05 |
Enrico Tassi | oldenv2newenv cache |
blob | commitdiff | raw | diff to current |
| 2008-02-05 |
Enrico Tassi | uri -> reference (2) |
blob | commitdiff | raw | diff to current |
| 2008-01-31 |
Wilmer Ricciotti | One Obj.magic implemented, trust changed to false. |
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