| 2008-07-23 |
Enrico Tassi | better tex/utf8 win |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | better cb |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | better UI for TeX/Unicode and terms grammar |
tree | commitdiff |
| 2008-07-23 |
Claudio Sacerdoti... | Update. |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | remove bad aliases from toolbox |
tree | commitdiff |
| 2008-07-23 |
Claudio Sacerdoti... | Universe levels fixed. |
tree | commitdiff |
| 2008-07-22 |
Ferruccio Guidi | matitadep: we now handle the inline of an uri, we remov... |
tree | commitdiff |
| 2008-07-22 |
Ferruccio Guidi | transcript: now we can generate procedural output |
tree | commitdiff |
| 2008-07-22 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-22 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | In some universe, membership is a morphism. |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | Sambin's & Valentini's toolbox (???) |
tree | commitdiff |
| 2008-07-22 |
Claudio Sacerdoti... | Dependencies removed. |
tree | commitdiff |
| 2008-07-21 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-21 |
Claudio Sacerdoti... | frac is an infix operator! |
tree | commitdiff |
| 2008-07-21 |
Ferruccio Guidi | we implemented the support for generating ma files... |
tree | commitdiff |
| 2008-07-21 |
Enrico Tassi | added notes about notation |
tree | commitdiff |
| 2008-07-21 |
Enrico Tassi | add conf key matita.debug_menu |
tree | commitdiff |
| 2008-07-21 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-07-21 |
Claudio Sacerdoti... | Semantic analysis implemented (sort of). |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | New input notation for bottom-up tree construction... |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | Snapshot. |
tree | commitdiff |
| 2008-07-18 |
Claudio Sacerdoti... | Input notation. |
tree | commitdiff |
| 2008-07-17 |
Claudio Sacerdoti... | Bugs fixed: |
tree | commitdiff |
| 2008-07-17 |
Claudio Sacerdoti... | 1 => \\e |
tree | commitdiff |
| 2008-07-16 |
Ferruccio Guidi | Procedural: some comments added in the generated script |
tree | commitdiff |
| 2008-07-16 |
Claudio Sacerdoti... | Duplicated doc removed. |
tree | commitdiff |
| 2008-07-16 |
Claudio Sacerdoti... | Snapshot (not working). |
tree | commitdiff |
| 2008-07-16 |
Claudio Sacerdoti... | a) update with upstream version |
tree | commitdiff |
| 2008-07-15 |
Ferruccio Guidi | cic2acic: new function acic_term_of_cic_term |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | more notation moved to core notation, unification of... |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | Since CProp_i = Type_i everything lowered without 2... |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | models over N fixed |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | new q_function representation |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | removed dummy comment |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | Using Prop conjuction on Props lowers the universes. |
tree | commitdiff |
| 2008-07-12 |
Ferruccio Guidi | librarian: retrieval of buildable files speeded up... |
tree | commitdiff |
| 2008-07-12 |
Claudio Sacerdoti... | New feature/bug fixed (hopefully): it is now possible... |
tree | commitdiff |
| 2008-07-12 |
Claudio Sacerdoti... | Notation for existential partially fixed: it is now... |
tree | commitdiff |
| 2008-07-11 |
Claudio Sacerdoti... | A very nice experiment using notation: we define the... |
tree | commitdiff |
| 2008-07-11 |
Claudio Sacerdoti... | Exists is no longer an ad-hoc notation hard-coded in... |
tree | commitdiff |
| 2008-07-11 |
Claudio Sacerdoti... | Added new ternary layout \infrule premises conclusion... |
tree | commitdiff |
| 2008-07-10 |
Enrico Tassi | value has a specification |
tree | commitdiff |
| 2008-07-10 |
Enrico Tassi | updated changelog |
tree | commitdiff |
| 2008-07-10 |
Enrico Tassi | more work on dama |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | better notation |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | minor fixes |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
tree | commitdiff |
| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info... |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | More definitions, following Ciraulo's Phd Thesis "Const... |
tree | commitdiff |
| 2008-07-04 |
Ferruccio Guidi | - Procedural: bug fix in rendering the application... |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | Compatibility finished. |
tree | commitdiff |
| 2008-07-04 |
Claudio Sacerdoti... | Nice: cotransitivity proved. |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | More work. |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | First few lemmas. But I have some problems in making... |
tree | commitdiff |
| 2008-07-03 |
Claudio Sacerdoti... | First experiment in Padua about formal topologies. |
tree | commitdiff |
| 2008-07-03 |
Enrico Tassi | ...snapshot |
tree | commitdiff |
| 2008-07-03 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | some work |
tree | commitdiff |
| 2008-07-02 |
Ferruccio Guidi | svn:ignore set on LambdaDelta-2 |
tree | commitdiff |
| 2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | return 1 in case of failure |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-01 |
Ferruccio Guidi | - lambda-delta: some speed up (not very much :) actually) |
tree | commitdiff |
| 2008-07-01 |
Enrico Tassi | shifting done, merge attacked |
tree | commitdiff |
| 2008-07-01 |
Enrico Tassi | shift almost done |
tree | commitdiff |
| 2008-06-30 |
Enrico Tassi | new specification |
tree | commitdiff |
| 2008-06-30 |
Enrico Tassi | some more work on q |
tree | commitdiff |
| 2008-06-28 |
Enrico Tassi | some more work to factorize out uninteresting parts... |
tree | commitdiff |
| 2008-06-27 |
Enrico Tassi | more work to try to understand where the issue is |
tree | commitdiff |
| 2008-06-27 |
Enrico Tassi | lost in the wood |
tree | commitdiff |
| 2008-06-26 |
Enrico Tassi | more work |
tree | commitdiff |
| 2008-06-26 |
Enrico Tassi | few more steps |
tree | commitdiff |
| 2008-06-26 |
Enrico Tassi | more work |
tree | commitdiff |
| 2008-06-26 |
Enrico Tassi | some more work |
tree | commitdiff |
| 2008-06-26 |
Enrico Tassi | more work on q |
tree | commitdiff |
| 2008-06-25 |
Enrico Tassi | some more work |
tree | commitdiff |
| 2008-06-25 |
Enrico Tassi | better, reparsable, notation |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | removed <_,_> notation second interpretation for depend... |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | more work, but russell too slow |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | notation support fixed to parentesize in a more sane... |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | xxx |
tree | commitdiff |
| 2008-06-22 |
Ferruccio Guidi | - grafiteParser.ml: the callback invocation was displaced |
tree | commitdiff |
| 2008-06-20 |
Enrico Tassi | left -> right |
tree | commitdiff |
| 2008-06-20 |
Claudio Sacerdoti... | Fixed bugs in the documentation of notation. |
tree | commitdiff |
| 2008-06-20 |
Claudio Sacerdoti... | More documentation for notation. |
tree | commitdiff |
| 2008-06-20 |
Claudio Sacerdoti... | Further documentation for notation. |
tree | commitdiff |
| 2008-06-20 |
Claudio Sacerdoti... | - partial implementation of pattern for case documented |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | fixed core notation |
tree | commitdiff |
| 2008-06-19 |
Claudio Sacerdoti... | - notation fixed according to the new stricter semantics |
tree | commitdiff |
| 2008-06-19 |
Ferruccio Guidi | - Procedural: we now check that an eliminator opens... |
tree | commitdiff |
| 2008-06-19 |
Enrico Tassi | notation on steroids: 'term 40 x' is a valid variable... |
tree | commitdiff |
| 2008-06-18 |
Claudio Sacerdoti... | interpretation documented |
tree | commitdiff |
| 2008-06-18 |
Enrico Tassi | removed unused variable |
tree | commitdiff |
| 2008-06-18 |
Enrico Tassi | some work on Q |
tree | commitdiff |
| next |
projects / helm.git / history