| 2008-06-09 |
Enrico Tassi | initial work on lebesque
|
commit | commitdiff | tree |
| 2008-06-09 |
Enrico Tassi | exhaustivity completed
|
commit | commitdiff | tree |
| 2008-06-09 |
Enrico Tassi | exhaustivity, some work
|
commit | commitdiff | tree |
| 2008-06-07 |
Enrico Tassi | exhaustivity defined
|
commit | commitdiff | tree |
| 2008-06-07 |
Enrico Tassi | proof simplified
|
commit | commitdiff | tree |
| 2008-06-06 |
Enrico Tassi | lemma 3.6 subverted
|
commit | commitdiff | tree |
| 2008-06-05 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2008-06-05 |
Enrico Tassi | added order_continuity
|
commit | commitdiff | tree |
| 2008-06-05 |
Enrico Tassi | sandwich is back
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | some work on uniformity
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | end of section 2.2
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | proof refactored
|
commit | commitdiff | tree |
| 2008-06-03 |
Enrico Tassi | xxx
|
commit | commitdiff | tree |
| 2008-06-01 |
Enrico Tassi | more work on supremum
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there!
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | irrelevance check half implemented but already impossible to
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | garbage removed
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | more work on dama
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | prod moved under lambda-prolog unification case
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | added CProp
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | thanks to the fact that we convert well typed term...
|
commit | commitdiff | tree |
| 2008-05-30 |
Enrico Tassi | added a bit more reduction in case Prod v.s. term,...
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | relevance check partially implemented but bugged since...
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | case not unfilding fixed
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | CProp, since it was defined in CoRN as a Type, is predicative.
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | 0.5.1 released
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | unused variables removed
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | ref sync check fixed controlling fix/cofix coherence
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | first page of the new dama proof
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-29 |
Enrico Tassi | the type of the match was obtained reducing the outtype
|
commit | commitdiff | tree |
| 2008-05-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-28 |
Enrico Tassi | dama restarted
|
commit | commitdiff | tree |
| 2008-05-28 |
Enrico Tassi | cleanup
|
commit | commitdiff | tree |
| 2008-05-28 |
Enrico Tassi | the attempt of completing dama using duality frozen
|
commit | commitdiff | tree |
| 2008-05-28 |
Enrico Tassi | 0.5.1
|
commit | commitdiff | tree |
| 2008-05-27 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-27 |
Enrico Tassi | smarter lexer needed by lambda-delta that is splitting...
|
commit | commitdiff | tree |
| 2008-05-27 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-27 |
Enrico Tassi | CoRN moved in contribs
|
commit | commitdiff | tree |
| 2008-05-27 |
Enrico Tassi | frst step to move away the CoRN stuff
|
commit | commitdiff | tree |
| 2008-05-27 |
Enrico Tassi | frst step to move away the CoRN stuff
|
commit | commitdiff | tree |
| 2008-05-27 |
Enrico Tassi | auto calls cleanup\
|
commit | commitdiff | tree |
| 2008-05-26 |
Enrico Tassi | better description of declarative tactics
|
commit | commitdiff | tree |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the...
|
commit | commitdiff | tree |
| 2008-05-26 |
Enrico Tassi | Universe.key was not used to index terms, but was used...
|
commit | commitdiff | tree |
| 2008-05-26 |
Enrico Tassi | added comment for zack
|
commit | commitdiff | tree |
| 2008-05-26 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-26 |
Enrico Tassi | auto syntax updated
|
commit | commitdiff | tree |
| 2008-05-26 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-24 |
Enrico Tassi | order of goals changes, open ones are preferred to...
|
commit | commitdiff | tree |
| 2008-05-21 |
Enrico Tassi | minimal implementation of left parameters display
|
commit | commitdiff | tree |
| 2008-05-21 |
Enrico Tassi | 0.5.1 should be realased soon, the bug that was affecting...
|
commit | commitdiff | tree |
| 2008-05-19 |
Enrico Tassi | added leftno to references f inductive types and constructor...
|
commit | commitdiff | tree |
| 2008-05-19 |
Enrico Tassi | added aps generation
|
commit | commitdiff | tree |
| 2008-05-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-05-19 |
Enrico Tassi | renamed add_le_constraint to add_constraint since it...
|
commit | commitdiff | tree |
| 2008-05-18 |
Enrico Tassi | run fsub during night
|
commit | commitdiff | tree |
| 2008-05-18 |
Enrico Tassi | names fixed accoding to the new ones generated after...
|
commit | commitdiff | tree |
| 2008-05-18 |
Enrico Tassi | revert last commit, context' -> context (added comment)
|
commit | commitdiff | tree |
| 2008-05-18 |
Enrico Tassi | using the right names in the context to check match...
|
commit | commitdiff | tree |
| 2008-05-17 |
Enrico Tassi | impredicative Set is considered as Prop in the new...
|
commit | commitdiff | tree |
| 2008-05-16 |
Enrico Tassi | ranking reports the lest of univs
|
commit | commitdiff | tree |
| 2008-05-16 |
Enrico Tassi | added new implementation of universes
|
commit | commitdiff | tree |
| 2008-05-16 |
Enrico Tassi | added name_of_uri
|
commit | commitdiff | tree |
| 2008-05-16 |
Enrico Tassi | meta VS meta in alpha_eq honors substitution
|
commit | commitdiff | tree |
| 2008-05-16 |
Enrico Tassi | used ind/coind information in references
|
commit | commitdiff | tree |
| 2008-05-16 |
Enrico Tassi | types where compared without lookig at test_eq_only
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | (Approximated) inference of relevance implemented:...
|
commit | commitdiff | tree |
| 2008-05-15 |
Enrico Tassi | First implementation of irrelevance in conversion.
|
commit | commitdiff | tree |
| 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 |
| next |
projects / helm.git / search