| 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 |
| 2008-04-11 |
Enrico Tassi | added a parameter to unshare universes
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | Conversion of 2 lambdas was not requiring equality...
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | context of types built in the reverse order
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | added a simplify to prevent the generation of an ugly fix
|
commit | commitdiff | tree |
| 2008-04-11 |
Enrico Tassi | implemented inductive and less parentheses
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | print unnamed variables as __n
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | switch off profilers
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | pp with parenthesis only when necessary and with some...
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | better pp in Appl
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | better pp
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | pretty printer on steroids
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | added profiling on/off
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | invalidate fixed
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | allow to switch profiling on and off on the fly
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | removed two useless calls to the environment, one still...
|
commit | commitdiff | tree |
| 2008-04-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-04-08 |
Enrico Tassi | added simplify to avoid ugly proofterm
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added invalidate to clear the cache and ease the comparison...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | commented out uris of objs that do not compile properly
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added comparison with old kernel
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | fixed error message for eat prods
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | invalidate
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | uris relative to axioms are translated in the right way
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added invalidate
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added preliminary checks for indtys
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | call get_obj instead of get_cooked_obj ~trust:false
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added case of const and axiom
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added # to comment
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | better printings
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | the explicit type in a LetIn must be typecheckd before...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | opt compilation enabled, removed some pps, check has...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | lefts_ad_tys properly sorted, added some metasenv here...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | lefts_and_tys was tys@lefts, CSC claims it was working...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added a list of uris to ease debugging
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | print the excpetion and raise it again, seems to produce...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | new constants have depth = max_int insted of 0 so that...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | off by one in calling count_from
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | fixed bug in translating Fix, recno was not properly...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | added a pretty printing of the new object and use argv...
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | context, metasenv and subst made mandatory in CicPp
|
commit | commitdiff | tree |
| 2008-04-07 |
Enrico Tassi | guarded by has a nice error message
|
commit | commitdiff | tree |
| next |
projects / helm.git / search