| 2008-05-15 |
Enrico Tassi | New function get_relevance and new (not exported) function...
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | New function list_forall_default3. 3 euros to the first...
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | Bug fixed in computation of heights: a constant must...
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | Implementation of calculation of heights.
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | Typo fixed.
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | Major code semplification and bugs removed (thanks...
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | height of constants properly handled
|
commit | commitdiff | tree |
| 2008-05-14 |
Enrico Tassi | partial implementation of reduction up to a given height
|
commit | commitdiff | tree |
| 2008-05-14 |
Enrico Tassi | fixed error message
|
commit | commitdiff | tree |
| 2008-05-13 |
Enrico Tassi | wrong test equality only fixed
|
commit | commitdiff | tree |
| 2008-05-13 |
Enrico Tassi | convertibility was taking a metasenv but not using it
|
commit | commitdiff | tree |
| 2008-05-12 |
Enrico Tassi | height is stored in the reference, no need to fetch...
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | fixed english
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | valid xml
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | released 0.5.0
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-10 |
Enrico Tassi | some files orphaned
|
commit | commitdiff | tree |
| 2008-05-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-09 |
Enrico Tassi | a missing prime
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | get_check_fix and cofix unified, bug regarding debruijnation...
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | get_checked_indtys can take a constructor reference
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | added mk_cofix
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | let corec
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | CoFix cache implemented
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | fix_left_in_constr still broken, ask enrico
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | guarded_by_constructors implemented, some cleanup here...
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | removed dead code
|
commit | commitdiff | tree |
| 2008-05-05 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-01 |
Enrico Tassi | tagging 0.5.0-rc1
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | added check on all bodies, only the one we actually...
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | added fake uri when the univ is anon
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | fixed wrong Rel, still to do: Fix(i,j) applied to dangerous...
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | universes are written with the URI inside objects,...
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | xml strict!
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | many pending modifications were there, now the website...
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | guarded_by_destructors on steroids
|
commit | commitdiff | tree |
| 2008-04-30 |
Enrico Tassi | added list_mapi
|
commit | commitdiff | tree |
| 2008-04-29 |
Enrico Tassi | speedup in fixing the graph closures
|
commit | commitdiff | tree |
| 2008-04-24 |
Enrico Tassi | guarded_by_constructor completely rewritten, fixed...
|
commit | commitdiff | tree |
| 2008-04-24 |
Enrico Tassi | added coinductive example
|
commit | commitdiff | tree |
| 2008-04-23 |
Enrico Tassi | ported the instantiate-left-params-to-calculate-rec...
|
commit | commitdiff | tree |
| 2008-04-22 |
Enrico Tassi | oblivion ugraph everywhere outside the kernel
|
commit | commitdiff | tree |
| 2008-04-22 |
Enrico Tassi | slow_implementation and some dead code removed
|
commit | commitdiff | tree |
| 2008-04-22 |
Enrico Tassi | more strict check by CSC, I miss it
|
commit | commitdiff | tree |
| 2008-04-22 |
Enrico Tassi | fix cache comparison relaxed to URI and not REFERENCE
|
commit | commitdiff | tree |
| 2008-04-22 |
Enrico Tassi | added a call to ppcontext in the case of appl, to ease...
|
commit | commitdiff | tree |
| 2008-04-22 |
Enrico Tassi | added ppcontext
|
commit | commitdiff | tree |
| 2008-04-21 |
Enrico Tassi | fix universe handling, newly encountered objects are...
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | better error message
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | impredicative set work around
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | impredicative set work around
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | associativity of -> fixed
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | ancient graph regarding universes and trust=false,...
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | extlib list_uniq instead of local copy
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | ranking function fixed: when graphs are collapsed one...
|
commit | commitdiff | tree |
| 2008-04-19 |
Enrico Tassi | added flag to change Set into Type on the fly, that...
|
commit | commitdiff | tree |
| 2008-04-18 |
Enrico Tassi | workaround for Pi associativity
|
commit | commitdiff | tree |
| 2008-04-18 |
Enrico Tassi | workaround for some Set/Type problems
|
commit | commitdiff | tree |
| 2008-04-18 |
Enrico Tassi | cicEnvironment refactoring with sound view of Coq`s...
|
commit | commitdiff | tree |
| 2008-04-18 |
Enrico Tassi | assertion was wrong, an object can contain a named...
|
commit | commitdiff | tree |
| 2008-04-18 |
Enrico Tassi | graph generation phase fixed
|
commit | commitdiff | tree |
| 2008-04-18 |
Enrico Tassi | Appl case in is_really_smaller fixed as in the old...
|
commit | commitdiff | tree |
| 2008-04-17 |
Enrico Tassi | example:
|
commit | commitdiff | tree |
| 2008-04-17 |
Enrico Tassi | added a missing whd
|
commit | commitdiff | tree |
| 2008-04-17 |
Enrico Tassi | new calculation of recursive parameters in guarded...
|
commit | commitdiff | tree |
| 2008-04-17 |
Enrico Tassi | Two similar cases packed together
|
commit | commitdiff | tree |
| 2008-04-17 |
Enrico Tassi | some fixes for guardness conditions
|
commit | commitdiff | tree |
| 2008-04-17 |
Enrico Tassi | is_really_smaller in sync with old kernel, impossible...
|
commit | commitdiff | tree |
| 2008-04-15 |
Enrico Tassi | get_checked_fix -> get_checked_fixes
|
commit | commitdiff | tree |
| 2008-04-15 |
Enrico Tassi | added comment
|
commit | commitdiff | tree |
| 2008-04-15 |
Enrico Tassi | positivity check fixed, a MutInd not applied (but with...
|
commit | commitdiff | tree |
| 2008-04-15 |
Enrico Tassi | do not use an implicit but a sort as a neutral term...
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | objects are typechecked to ensure there is a graph...
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | leftno should be increased of the expnamedsubst, but...
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | better error message
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | same_obj made more precise, fixed the order of the...
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | ficed fixpoint cache usage for mutual fix
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | fixed positivity conditions
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | added mk_fix i j r that given an r of a fix generated...
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | positivity condition was relying on the name declared...
|
commit | commitdiff | tree |
| 2008-04-14 |
Enrico Tassi | added little optimization to not add twice the same arc
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | quinck and untested implementation of positivity conditions...
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | added depndency of new kernel to metadata to allow...
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | FIXED bug, added assertion in case a universe inside...
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | added function to fresh types
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | call Unshare.fresh_types
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | load the graph of objects that depend on the ones requested,
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | use universe rank instead of Type0
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | Type related failures fixed
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | better pp of objects
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | removed useless file
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | fixed modules order
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | more fix removed from types
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | more fix removed from types in proofs
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | when we build the elimination principle we fresh universes...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search