| 2008-09-26 |
Enrico Tassi | more push/pop to avoid confusion with imperative data... |
tree | commitdiff |
| 2008-09-26 |
Ferruccio Guidi | Procedural: we removed some commented code |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | include statement better implemented: |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | auto was compiraing lazy proof terms with = ... fixed |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | iremoved call to auto |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | lazy proof term to increase sharing and decrease memory... |
tree | commitdiff |
| 2008-09-25 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-25 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-25 |
Enrico Tassi | ... |
tree | commitdiff |
| 2008-09-25 |
Enrico Tassi | beta expand |
tree | commitdiff |
| 2008-09-25 |
Enrico Tassi | ... |
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-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-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 |
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 |
| next |
projects / helm.git / history