| 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 |
| 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 |
| next |
projects / helm.git / search