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 |
2008-05-21 |
Enrico Tassi | 0.5.1 should be realased soon, the bug that was affecti... |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | Here is where we should add relevance checks. |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | Bug fixed in computation of leftnos: variables were... |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | Code simplification. |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | Added cprop <= type constraint. |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | We do not need to give cprop a special status yet. |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | CProp dropped in favour of a cprop universe exported... |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Enrico Tassi | added leftno to references f inductive types and constr... |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Enrico Tassi | added aps generation |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
2008-05-19 |
Enrico Tassi | renamed add_le_constraint to add_constraint since it... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | ... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Enrico Tassi | run fsub during night |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Bug fixed: when computing the left arguments, I was... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Enrico Tassi | names fixed accoding to the new ones generated after... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Enrico Tassi | revert last commit, context' -> context (added comment) |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Enrico Tassi | using the right names in the context to check match... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | New missing check implemented: the left parameters... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductiv... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Dummy dependent products in inductive types arities... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | This commit avoids cleaning dummy dependent types in... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Implemented translation of inductive types from the... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Serious bug fixed: the max of two universes was compute... |
commit | commitdiff | tree | snapshot |
2008-05-18 |
Claudio Sacerdoti... | Synch with the paper. |
commit | commitdiff | tree | snapshot |
next |