2008-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-24 |
Enrico Tassi | added skip function |
tree | commitdiff |
2008-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-24 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-22 |
Enrico Tassi | new iterator |
tree | commitdiff |
2008-09-22 |
Ferruccio Guidi | new small devel |
tree | commitdiff |
2008-09-22 |
Enrico Tassi | fixed auto invocation |
tree | commitdiff |
2008-09-21 |
Ferruccio Guidi | we commented some of the debug pps rather than removing... |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | snapshot |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | snapshot, cicMsubst compiles |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | more abstract discrimination tree |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | added list_seq |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | snapshot |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | better abstraction to allow 1 discrimination tree imple... |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | new discrimination tree |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | Revised discrimination tree implementation: |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | more comments and compare function for URI exported |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | removed debug pps |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | new reorganization |
tree | commitdiff |
2008-09-19 |
Enrico Tassi | fixed |
tree | commitdiff |
2008-09-19 |
Andrea Asperti | A temporary patch to demodulation theorem. |
tree | commitdiff |
2008-09-18 |
Enrico Tassi | removed debug pps |
tree | commitdiff |
2008-09-18 |
Ferruccio Guidi | applyTransformation: improved error detection |
tree | commitdiff |
2008-09-18 |
Ferruccio Guidi | librarian: improved error detection, bug fix in time... |
tree | commitdiff |
2008-09-18 |
Claudio Sacerdoti... | ppterm_in_named_context removed in favour of the high... |
tree | commitdiff |
2008-09-18 |
Claudio Sacerdoti... | Major reordering of theorems in the appropriate files. |
tree | commitdiff |
2008-09-18 |
Claudio Sacerdoti... | In case of coercion to Prod, the error message shown... |
tree | commitdiff |
2008-09-18 |
Enrico Tassi | fixed script |
tree | commitdiff |
2008-09-18 |
Claudio Sacerdoti... | Precedence level of \downarrow changed to match that... |
tree | commitdiff |
2008-09-17 |
Enrico Tassi | snapshot |
tree | commitdiff |
2008-09-17 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-16 |
Claudio Sacerdoti... | formal_map now defined |
tree | commitdiff |
2008-09-16 |
Claudio Sacerdoti... | Definition of formal_topologies. |
tree | commitdiff |
2008-09-16 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-16 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-16 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-16 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-16 |
Enrico Tassi | new directory for the newGeneration refiner |
tree | commitdiff |
2008-09-15 |
Claudio Sacerdoti... | BTop is a category. |
tree | commitdiff |
2008-09-12 |
Ferruccio Guidi | old bug in mtime computation fixed |
tree | commitdiff |
2008-09-12 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2008-09-12 |
Claudio Sacerdoti... | 1) as usual, I took the reverse notation for composition. |
tree | commitdiff |
2008-09-11 |
Claudio Sacerdoti... | helm mailing list moved to cs.unibo.it |
tree | commitdiff |
2008-09-10 |
Ferruccio Guidi | we skip discharging on matita opbjects (they don't... |
tree | commitdiff |
2008-09-10 |
Ferruccio Guidi | cicDischarge, Procedural: we improved debugging and... |
tree | commitdiff |
2008-09-10 |
Enrico Tassi | reverted auto experiment |
tree | commitdiff |
2008-09-10 |
Enrico Tassi | AGAIN A TEST |
tree | commitdiff |
2008-09-10 |
Enrico Tassi | COMMIT TO JUST RUN A BENCH, SHOULD BE REVERTED ASAP... |
tree | commitdiff |
2008-09-09 |
Claudio Sacerdoti... | Reordering of lemmas in proper places. |
tree | commitdiff |
2008-09-09 |
Claudio Sacerdoti... | Concrete spaces do form a category, after all :-) |
tree | commitdiff |
2008-09-09 |
Enrico Tassi | some work to make tries "printable", fixed comparison... |
tree | commitdiff |
2008-09-09 |
Claudio Sacerdoti... | Getting closer thanks to more technical arrangements. |
tree | commitdiff |
2008-09-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2008-09-08 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-08 |
Claudio Sacerdoti... | Concrete spaces now defined. |
tree | commitdiff |
2008-09-08 |
Claudio Sacerdoti... | Case c1 t1 vs c2 t2 where c1 and c2 are not splitted... |
tree | commitdiff |
2008-09-07 |
Ferruccio Guidi | cicDischarge: we still have some problems here. Some... |
tree | commitdiff |
2008-09-06 |
Ferruccio Guidi | we always save the discharged object for future reference |
tree | commitdiff |
2008-09-05 |
Ferruccio Guidi | we have to remove the Num directory :) |
tree | commitdiff |
2008-09-05 |
Ferruccio Guidi | transcript: we now check for non-existing objects |
tree | commitdiff |
2008-09-05 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-05 |
Enrico Tassi | unification+pullback fix. It used to saturate a coercio... |
tree | commitdiff |
2008-09-04 |
Ferruccio Guidi | transcript: improved debuugging facilities |
tree | commitdiff |
2008-09-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2008-09-04 |
Ferruccio Guidi | we forgot to delete the old CoRN mma files :) |
tree | commitdiff |
2008-09-04 |
Ferruccio Guidi | transcript: we improved the parser/lexer to read the... |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | fixed case of divergence |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | fixed notation |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | restored |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | .... |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-04 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | removed debug pps |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | comparison function fixed |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | ... |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | removed old non-working file |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | notation_id were compared using Pervasives.equal this... |
tree | commitdiff |
2008-09-04 |
Enrico Tassi | stop running LAMBDA-TYPES as a test, can be reactivated... |
tree | commitdiff |
2008-09-04 |
Claudio Sacerdoti... | hbox => hvbox in constructor arguments in match patterns. |
tree | commitdiff |
2008-09-03 |
Claudio Sacerdoti... | Setoids are now more pervasive. |
tree | commitdiff |
2008-09-02 |
Claudio Sacerdoti... | Uri ending in '' were not accepted. Fixed. |
tree | commitdiff |
2008-09-01 |
Claudio Sacerdoti... | new debugging option |
tree | commitdiff |
2008-08-31 |
Claudio Sacerdoti... | Relations are now closer to Sambin's ones. I.e. they... |
tree | commitdiff |
2008-08-28 |
Enrico Tassi | ... |
tree | commitdiff |
2008-08-28 |
Enrico Tassi | ... |
tree | commitdiff |
2008-08-28 |
Ferruccio Guidi | new baseuri for procedural CoRN |
tree | commitdiff |
2008-08-28 |
Ferruccio Guidi | applyTransformation: variable discharging in procedural... |
tree | commitdiff |
2008-08-28 |
Ferruccio Guidi | cicDischarge: new module for discharging the explicit... |
tree | commitdiff |
2008-08-27 |
Claudio Sacerdoti... | Convergence is now defined. |
tree | commitdiff |
2008-08-27 |
Claudio Sacerdoti... | Better notation, in particular for subset comprehension. |
tree | commitdiff |
2008-08-26 |
Claudio Sacerdoti... | Notation |.| moved to core_notation. |
tree | commitdiff |
2008-08-26 |
Enrico Tassi | fixed some stuff |
tree | commitdiff |
2008-08-25 |
Ferruccio Guidi | bug fix in inline syntax |
tree | commitdiff |
2008-08-25 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
2008-08-25 |
Claudio Sacerdoti... | New categories REL and BP. |
tree | commitdiff |
2008-08-25 |
Claudio Sacerdoti... | New cool "type-checking" notation using colors and... |
tree | commitdiff |
2008-08-25 |
Claudio Sacerdoti... | Do not mess with my window manager: the Cic Browsers... |
tree | commitdiff |
2008-08-25 |
Claudio Sacerdoti... | Non-linear patterns are now allowed in notations. |
tree | commitdiff |
next |