2008-06-12 |
Enrico Tassi | fixed some regressions |
commit | commitdiff | tree | snapshot |
2008-06-11 |
Claudio Sacerdoti... | New, much faster implementation of factorize. |
commit | commitdiff | tree | snapshot |
2008-06-11 |
Enrico Tassi | gran casino |
commit | commitdiff | tree | snapshot |
2008-06-11 |
Enrico Tassi | meta not considered before in outtype |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | bla bla bla |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Wilmer Ricciotti | relevance check for Match |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | initial qork for models |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Wilmer Ricciotti | Added check of relevance lists for inductive types... |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | lebesgue proved |
commit | commitdiff | tree | snapshot |
2008-06-10 |
Enrico Tassi | snapshot |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Claudio Sacerdoti... | Most of the time, URIs can now be replaced with identif... |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Claudio Sacerdoti... | It is now possible to use identifiers in place of URI... |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Wilmer Ricciotti | Reverting to the previous version some files which... |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Wilmer Ricciotti | more proof irrelevance |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Enrico Tassi | initial work on lebesque |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Enrico Tassi | exhaustivity completed |
commit | commitdiff | tree | snapshot |
2008-06-09 |
Enrico Tassi | exhaustivity, some work |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required by elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | Generalize no more required for elim. |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more required before elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | generalize no more useful for elim |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | Bug fixed: wrong default pattern for generalize. |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | New: pattern for elim documented. |
commit | commitdiff | tree | snapshot |
2008-06-08 |
Claudio Sacerdoti... | Hypotheses patterns for elim implemented. No more need... |
commit | commitdiff | tree | snapshot |
2008-06-07 |
Enrico Tassi | exhaustivity defined |
commit | commitdiff | tree | snapshot |
2008-06-07 |
Enrico Tassi | proof simplified |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | Even more Q stuff moved around. |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | Even more Q stuff classified. |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Enrico Tassi | lemma 3.6 subverted |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | more stuff moved around |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | More Q stuff organized in a coherent way. |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | First snapshot at trying to clean up the Q library. |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Andrea Asperti | A new theorem |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Andrea Asperti | cleanup |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Andrea Asperti | Cleanup. |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | sieve.ma now depends only on primes.ma |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Andrea Asperti | Added frac.ma |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Andrea Asperti | Added Qplus_andrea.ma |
commit | commitdiff | tree | snapshot |
2008-06-06 |
Claudio Sacerdoti... | Reduce reduction tactic got rid of a long time ago. |
commit | commitdiff | tree | snapshot |
2008-06-05 |
Claudio Sacerdoti... | Eratosthene's sieve factorized out of nat/bertrand... |
commit | commitdiff | tree | snapshot |
2008-06-05 |
Enrico Tassi | .... |
commit | commitdiff | tree | snapshot |
2008-06-05 |
Enrico Tassi | added order_continuity |
commit | commitdiff | tree | snapshot |
2008-06-05 |
Enrico Tassi | sandwich is back |
commit | commitdiff | tree | snapshot |
2008-06-04 |
Wilmer Ricciotti | Proof-irrelevance check for all applications (first... |
commit | commitdiff | tree | snapshot |
2008-06-04 |
Wilmer Ricciotti | incomplete irrelevance test commented out |
commit | commitdiff | tree | snapshot |
2008-06-03 |
Claudio Sacerdoti... | Some proofs on enumerator and denominator. |
commit | commitdiff | tree | snapshot |
2008-06-03 |
Claudio Sacerdoti... | More work on rational numbers with unique representations. |
commit | commitdiff | tree | snapshot |
2008-06-03 |
Enrico Tassi | some work on uniformity |
commit | commitdiff | tree | snapshot |
2008-06-03 |
Enrico Tassi | end of section 2.2 |
commit | commitdiff | tree | snapshot |
2008-06-03 |
Enrico Tassi | proof refactored |
commit | commitdiff | tree | snapshot |
2008-06-03 |
Enrico Tassi | xxx |
commit | commitdiff | tree | snapshot |
2008-06-01 |
Enrico Tassi | more work on supremum |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | irrelevance check half implemented but already impossib... |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | garbage removed |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | more work on dama |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | prod moved under lambda-prolog unification case |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | added CProp |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | thanks to the fact that we convert well typed term... |
commit | commitdiff | tree | snapshot |
2008-05-30 |
Enrico Tassi | added a bit more reduction in case Prod v.s. term,... |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | relevance check partially implemented but bugged since... |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | case not unfilding fixed |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | CProp, since it was defined in CoRN as a Type, is predi... |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | 0.5.1 released |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | unused variables removed |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | ref sync check fixed controlling fix/cofix coherence |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | first page of the new dama proof |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-29 |
Enrico Tassi | the type of the match was obtained reducing the outtype |
commit | commitdiff | tree | snapshot |
2008-05-28 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-28 |
Enrico Tassi | dama restarted |
commit | commitdiff | tree | snapshot |
2008-05-28 |
Enrico Tassi | cleanup |
commit | commitdiff | tree | snapshot |
2008-05-28 |
Enrico Tassi | the attempt of completing dama using duality frozen |
commit | commitdiff | tree | snapshot |
2008-05-28 |
Enrico Tassi | 0.5.1 |
commit | commitdiff | tree | snapshot |
2008-05-27 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-27 |
Enrico Tassi | smarter lexer needed by lambda-delta that is splitting... |
commit | commitdiff | tree | snapshot |
2008-05-27 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-27 |
Enrico Tassi | CoRN moved in contribs |
commit | commitdiff | tree | snapshot |
2008-05-27 |
Enrico Tassi | frst step to move away the CoRN stuff |
commit | commitdiff | tree | snapshot |
2008-05-27 |
Enrico Tassi | frst step to move away the CoRN stuff |
commit | commitdiff | tree | snapshot |
2008-05-27 |
Enrico Tassi | auto calls cleanup\ |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Enrico Tassi | better description of declarative tactics |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Enrico Tassi | Universe.key was not used to index terms, but was used... |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Ferruccio Guidi | better presentation of lambda-delta |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Ferruccio Guidi | - some bugs fixed in the domain-based preorders on... |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Enrico Tassi | added comment for zack |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Enrico Tassi | auto syntax updated |
commit | commitdiff | tree | snapshot |
2008-05-26 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-24 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-24 |
Enrico Tassi | order of goals changes, open ones are preferred to... |
commit | commitdiff | tree | snapshot |
2008-05-21 |
Enrico Tassi | minimal implementation of left parameters display |
commit | commitdiff | tree | snapshot |
next |