| 2008-04-19 |
Enrico Tassi | impredicative set work around |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | associativity of -> fixed |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | ancient graph regarding universes and trust=false,... |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | extlib list_uniq instead of local copy |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | ranking function fixed: when graphs are collapsed one... |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | added flag to change Set into Type on the fly, that... |
tree | commitdiff |
| 2008-04-19 |
Claudio Sacerdoti... | oblivion_ugraph => empty_ugraph |
tree | commitdiff |
| 2008-04-19 |
Claudio Sacerdoti... | Added to flags to activate/disactivate pretty-printing... |
tree | commitdiff |
| 2008-04-19 |
Claudio Sacerdoti... | Uris must be stripped of their xpointers. |
tree | commitdiff |
| 2008-04-18 |
Claudio Sacerdoti... | Dead code removed. |
tree | commitdiff |
| 2008-04-18 |
Claudio Sacerdoti... | Inversion lemma for Forall. |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | workaround for Pi associativity |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | workaround for some Set/Type problems |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | cicEnvironment refactoring with sound view of Coq`s... |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | assertion was wrong, an object can contain a named... |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | graph generation phase fixed |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | Appl case in is_really_smaller fixed as in the old... |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | example: |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | added a missing whd |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | new calculation of recursive parameters in guarded... |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | Two similar cases packed together |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | some fixes for guardness conditions |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | is_really_smaller in sync with old kernel, impossible... |
tree | commitdiff |
| 2008-04-15 |
Claudio Sacerdoti... | check_is_really_smaller simplified to consider that... |
tree | commitdiff |
| 2008-04-15 |
Claudio Sacerdoti... | 1. bug fixed: the context must be type-checked before... |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | get_checked_fix -> get_checked_fixes |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | added comment |
tree | commitdiff |
| 2008-04-15 |
Claudio Sacerdoti... | added sample of guarded by in which coq is stronger |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | positivity check fixed, a MutInd not applied (but with... |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | do not use an implicit but a sort as a neutral term... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | objects are typechecked to ensure there is a graph... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | leftno should be increased of the expnamedsubst, but... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | better error message |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | same_obj made more precise, fixed the order of the... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | ficed fixpoint cache usage for mutual fix |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | fixed positivity conditions |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | added mk_fix i j r that given an r of a fix generated... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | positivity condition was relying on the name declared... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | added little optimization to not add twice the same arc |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | quinck and untested implementation of positivity condit... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | added depndency of new kernel to metadata to allow... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | FIXED bug, added assertion in case a universe inside... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | added function to fresh types |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | call Unshare.fresh_types |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | load the graph of objects that depend on the ones reque... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | use universe rank instead of Type0 |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | Type related failures fixed |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | better pp of objects |
tree | commitdiff |
| 2008-04-11 |
Claudio Sacerdoti... | Extracted code. The main executable is medium_tests... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | removed useless file |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | fixed modules order |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | more fix removed from types |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | more fix removed from types in proofs |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | when we build the elimination principle we fresh univer... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | added a parameter to unshare universes |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | Conversion of 2 lambdas was not requiring equality... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | context of types built in the reverse order |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | added a simplify to prevent the generation of an ugly fix |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | implemented inductive and less parentheses |
tree | commitdiff |
| 2008-04-10 |
Claudio Sacerdoti... | The cache of objects is now used also for cofixpoints. |
tree | commitdiff |
| 2008-04-10 |
Claudio Sacerdoti... | New: cache of translated fixpoints (to avoid the genera... |
tree | commitdiff |
| 2008-04-10 |
Claudio Sacerdoti... | does_not_occur exported to be used in oCic2NCic |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Bug fixed: references to CoFix are CoFix, not Fix. |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | print unnamed variables as __n |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | switch off profilers |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | pp with parenthesis only when necessary and with some... |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Fixed serious bug that occurred only in the following... |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | better pp in Appl |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | better pp |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | pretty printer on steroids |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Added some "\n" here and there to the pretty-printing... |
tree | commitdiff |
| 2008-04-09 |
Claudio Sacerdoti... | Grave bug fixed: Ce that point to definitions were... |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | added profiling on/off |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | invalidate fixed |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | allow to switch profiling on and off on the fly |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | removed two useless calls to the environment, one still... |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Variables are no longer experted (cooking is now implem... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Swapped arguments in error message. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Variables having a body can occur in cooked terms and... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Fix over the previous one: Var-LetIn abstractions shoul... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Error message improved. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Cooking w.r.t. variables with bodies is now implemented... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Fix name capture in cofix. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | To test the translation. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Name capture fixed. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Improved error messages in place of "sort elimination... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Seed reset before each convert_obj. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Use seed to avoid further name clashes. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Incredible, but true! Our name mangling clashed with... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Cooked objects are no longer well typed in the uncooked... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Improved eat_prods error message (at the cost of passin... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | The old kernel does not accept ens whose order is diffe... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Bad alpha-conversion by Enrico fixed. |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Bug fixed: the ens need not be ordered w.r.t. the decla... |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | j off by one in error message |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | fix_outty partially fixed: missing lifts in args and ens |
tree | commitdiff |
| next |
projects / helm.git / history