| 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 |
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 | 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... | In case of coercion to Prod, the error message shown... |
tree | commitdiff |
| 2008-09-17 |
Enrico Tassi | snapshot |
tree | commitdiff |
| 2008-09-17 |
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 | ... |
tree | commitdiff |
| 2008-09-16 |
Enrico Tassi | new directory for the newGeneration refiner |
tree | commitdiff |
| 2008-09-12 |
Ferruccio Guidi | old bug in mtime computation fixed |
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 |
Enrico Tassi | some work to make tries "printable", fixed comparison... |
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 | transcript: we now check for non-existing objects |
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 |
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 | removed debug pps |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | comparison function fixed |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | notation_id were compared using Pervasives.equal this... |
tree | commitdiff |
| 2008-09-04 |
Claudio Sacerdoti... | hbox => hvbox in constructor arguments in match patterns. |
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-28 |
Ferruccio Guidi | cicDischarge: new module for discharging the explicit... |
tree | commitdiff |
| 2008-08-25 |
Ferruccio Guidi | bug fix in inline syntax |
tree | commitdiff |
| 2008-08-25 |
Claudio Sacerdoti... | Non-linear patterns are now allowed in notations. |
tree | commitdiff |
| 2008-08-25 |
Ferruccio Guidi | transcript: bug fix in the generation of axioms |
tree | commitdiff |
| 2008-08-23 |
Ferruccio Guidi | Procedural: bug fix in comment generation |
tree | commitdiff |
| 2008-08-23 |
Ferruccio Guidi | Procedural: explicit flavour specification for constant... |
tree | commitdiff |
| 2008-08-23 |
Enrico Tassi | notation with mstyle attributes, like colors and size |
tree | commitdiff |
| 2008-08-21 |
Claudio Sacerdoti... | Avoid warning. |
tree | commitdiff |
| 2008-08-21 |
Claudio Sacerdoti... | Added catching of an exception to implement a missing... |
tree | commitdiff |
| 2008-08-21 |
Ferruccio Guidi | basic support for imposed flavour in procedural object... |
tree | commitdiff |
| 2008-08-12 |
Wilmer Ricciotti | Fixed two legacy comments |
tree | commitdiff |
| 2008-08-01 |
Enrico Tassi | fixed recursiveness check |
tree | commitdiff |
| 2008-08-01 |
Enrico Tassi | fixed recursiveness check |
tree | commitdiff |
| 2008-07-30 |
Enrico Tassi | fixed check, if 0 constructors then no List.nth is... |
tree | commitdiff |
| 2008-07-30 |
Enrico Tassi | allowed sort elim now check for recursive types |
tree | commitdiff |
| 2008-07-30 |
Enrico Tassi | fixed allowed sort elim |
tree | commitdiff |
| 2008-07-30 |
Claudio Sacerdoti... | Missing check implemented: uniformity of left parameter... |
tree | commitdiff |
| 2008-07-30 |
Claudio Sacerdoti... | Missing check in positivity implemented: we did not... |
tree | commitdiff |
| 2008-07-25 |
Enrico Tassi | - too strict check on left parameters of constructors... |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | positivity check fixed |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | positivity check fixed, some subterms were erroneously... |
tree | commitdiff |
| 2008-07-23 |
Enrico Tassi | better ranking interface |
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-21 |
Claudio Sacerdoti... | Error message improved. |
tree | commitdiff |
| 2008-07-21 |
Claudio Sacerdoti... | Rendering of \infrule improved. |
tree | commitdiff |
| 2008-07-21 |
Ferruccio Guidi | we implemented the support for generating ma files... |
tree | commitdiff |
| 2008-07-21 |
Enrico Tassi | avoid empty hvbox |
tree | commitdiff |
| 2008-07-18 |
Enrico Tassi | better metavariable context |
tree | commitdiff |
| 2008-07-18 |
Enrico Tassi | metavariable context has a separator now |
tree | commitdiff |
| 2008-07-18 |
Enrico Tassi | exception inside regex callback not re-raised if equal... |
tree | commitdiff |
| 2008-07-17 |
Claudio Sacerdoti... | Bugs fixed: |
tree | commitdiff |
| 2008-07-16 |
Ferruccio Guidi | Procedural: some comments added in the generated script |
tree | commitdiff |
| 2008-07-16 |
Enrico Tassi | notations for lists adds some breaking points |
tree | commitdiff |
| 2008-07-15 |
Ferruccio Guidi | cic2acic: new function acic_term_of_cic_term |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | CProp_i <= Type_i , Type_i <= CProp_i |
tree | commitdiff |
| 2008-07-14 |
Ferruccio Guidi | lambda-delta: we added the support for position indexes... |
tree | commitdiff |
| 2008-07-14 |
Ferruccio Guidi | Procedural: we added the support for rendering definiti... |
tree | commitdiff |
| 2008-07-13 |
Ferruccio Guidi | Procedural: we added the support for theorem flavours... |
tree | commitdiff |
| 2008-07-13 |
Ferruccio Guidi | cicUtil : we added a context to is_sober... |
tree | commitdiff |
| 2008-07-12 |
Ferruccio Guidi | Procedural: bug fix in the procedural rendering of... |
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-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 | fixed regression in casting an argument to funclass... |
tree | commitdiff |
| 2008-07-09 |
Ferruccio Guidi | some bug fixes |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | tab -> ' ' |
tree | commitdiff |
| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info... |
tree | commitdiff |
| 2008-07-04 |
Ferruccio Guidi | - we replaced a normalize with a whd in the classificat... |
tree | commitdiff |
| 2008-07-04 |
Ferruccio Guidi | - Procedural: bug fix in rendering the application... |
tree | commitdiff |
| 2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
tree | commitdiff |
| 2008-07-02 |
Wilmer Ricciotti | Fixed a bug which prevented mutually recursive definiti... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | calculation of the sort user to choose the rewriting... |
tree | commitdiff |
| 2008-06-25 |
Enrico Tassi | better, reparsable, notation |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | notation factored, coercion commant taking terms and... |
tree | commitdiff |
| 2008-06-24 |
Enrico Tassi | missing file added |
tree | commitdiff |
| 2008-06-23 |
Enrico Tassi | add \\ in front of tex macros |
tree | commitdiff |
| next |
projects / helm.git / history