| 2009-09-02 |
Enrico Tassi | do not fail if the inductive type is mutual, just do... |
tree | commitdiff |
| 2009-09-02 |
Enrico Tassi | decent error on interpretation declaration |
tree | commitdiff |
| 2009-09-01 |
Enrico Tassi | fix double app in Ast |
tree | commitdiff |
| 2009-09-01 |
Enrico Tassi | better print of ILLEGAL applications |
tree | commitdiff |
| 2009-09-01 |
Enrico Tassi | catch wrapped exception |
tree | commitdiff |
| 2009-08-25 |
Enrico Tassi | ncoindutive now generates a co-inductive type, not... |
tree | commitdiff |
| 2009-08-25 |
Enrico Tassi | Meta case not handled, the iterator was complaining. |
tree | commitdiff |
| 2009-08-14 |
Claudio Sacerdoti... | Since the introduction of saturation, an assert false... |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | Some quick patch to fix elimination that used to look for |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | fix_sorts (cfr. previous commit) used to break too... |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | Assert false do not allow to debug... |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | Let's refresh the universe to avoid assert failure. |
tree | commitdiff |
| 2009-08-06 |
Claudio Sacerdoti... | Metas must be handled when using iterators. |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | Bad patch reverted (in error message). |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | Bug fixed: one case of too many arguments was not detec... |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | Serious bug fixed: uris were not refreshed when loading... |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | Record projections are now defined as fixpoints in... |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | \ldots are now used in nelim and ncases |
tree | commitdiff |
| 2009-07-31 |
Claudio Sacerdoti... | Pp fixed in order to obtain read-back. |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | napply now automatically inserts \ldots at the end |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | First implementation of \ldots. |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | Don't reinvent the wheel. |
tree | commitdiff |
| 2009-07-29 |
Andrea Asperti | New demodulation (innermost, optimized to avoid reducin... |
tree | commitdiff |
| 2009-07-29 |
Andrea Asperti | Changed the ordering of rels, and the introduction... |
tree | commitdiff |
| 2009-07-29 |
Andrea Asperti | Lazy strings |
tree | commitdiff |
| 2009-07-29 |
Andrea Asperti | Added the benchmark with the new demodulation function. |
tree | commitdiff |
| 2009-07-28 |
Claudio Sacerdoti... | "..." -> "\ldots" for implicit vectors |
tree | commitdiff |
| 2009-07-28 |
Claudio Sacerdoti... | 1) Some more work for vector implicits. |
tree | commitdiff |
| 2009-07-28 |
Claudio Sacerdoti... | Introduction of vectors of implicit (only for NG). |
tree | commitdiff |
| 2009-07-28 |
denes | New reference benchmark with CPU Time |
tree | commitdiff |
| 2009-07-27 |
denes | Removed meaningless time information |
tree | commitdiff |
| 2009-07-27 |
denes | Removed internal default timeout |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | Stupid bug fixed: the test to detect Uncertain cases... |
tree | commitdiff |
| 2009-07-27 |
denes | Removed old logs |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | Serious bug fixed: because of lazy evaluation of !requi... |
tree | commitdiff |
| 2009-07-27 |
denes | Moved benchmarks to new folder |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | Debugging code removed. |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | Record fields declared as coercions as now really decla... |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | Beta-expansion was avoided as soon as one argument... |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | Function to map NCic.term to CicNotationPt.term finished. |
tree | commitdiff |
| 2009-07-24 |
Claudio Sacerdoti... | Bug (found during code review) fixed (but not tested... |
tree | commitdiff |
| 2009-07-22 |
Claudio Sacerdoti... | Major speed-up: meta-chains are now expanded during... |
tree | commitdiff |
| 2009-07-22 |
denes | Fixed test for invertibility |
tree | commitdiff |
| 2009-07-22 |
denes | Now using lazy strings for debug printings |
tree | commitdiff |
| 2009-07-22 |
Claudio Sacerdoti... | leftno was List.length rights :-) |
tree | commitdiff |
| 2009-07-22 |
Claudio Sacerdoti... | Almost ready to implement coercion declaration for... |
tree | commitdiff |
| 2009-07-21 |
Claudio Sacerdoti... | Debugging code removed. |
tree | commitdiff |
| 2009-07-21 |
Claudio Sacerdoti... | Record projections are now automatically generated... |
tree | commitdiff |
| 2009-07-21 |
denes | Implemented handling of Invertible equalities |
tree | commitdiff |
| 2009-07-20 |
Enrico Tassi | sorted modules |
tree | commitdiff |
| 2009-07-20 |
Claudio Sacerdoti... | Debugging printf removed |
tree | commitdiff |
| 2009-07-20 |
Claudio Sacerdoti... | nrewrite now uses the appropriate principle when going... |
tree | commitdiff |
| 2009-07-20 |
denes | Removed status printing by processes |
tree | commitdiff |
| 2009-07-20 |
denes | Fixed multiple printing |
tree | commitdiff |
| 2009-07-20 |
Wilmer Ricciotti | Final version, submitted to CASC-22. |
tree | commitdiff |
| 2009-07-20 |
Wilmer Ricciotti | added a flag for age selection |
tree | commitdiff |
| 2009-07-20 |
Claudio Sacerdoti... | Very serious bug fixed in unification, but the fix... |
tree | commitdiff |
| 2009-07-20 |
Claudio Sacerdoti... | 1) The NG kernel now accepts only usage of declared... |
tree | commitdiff |
| 2009-07-20 |
denes | One-side indexing for commutativity |
tree | commitdiff |
| 2009-07-20 |
denes | No demod call on functionnal symbols |
tree | commitdiff |
| 2009-07-20 |
Claudio Sacerdoti... | 1) ppmetasenv and ppcontext to reduce the amount of... |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | nelim now uses the appropriate _rect_XXX elimination... |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | 1) the user is notified when a new object is defined |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | More info to refine empty types elimination. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Generation of principles is now atomic. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Debugging code commented out. |
tree | commitdiff |
| 2009-07-17 |
Enrico Tassi | add comment |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Bug fixed: singleton application. |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | New suffixes for elimination principles: |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | 1) added a function to retrieve all the universes curre... |
tree | commitdiff |
| 2009-07-17 |
Claudio Sacerdoti... | Generation of inductive principle for Type[0]. |
tree | commitdiff |
| 2009-07-16 |
denes | Sorted version of eligible problems list |
tree | commitdiff |
| 2009-07-16 |
denes | Disabled age selection and ad hoc goal weight computation |
tree | commitdiff |
| 2009-07-15 |
Enrico Tassi | ncopy partially implemented and fixed (a ?) chain to... |
tree | commitdiff |
| 2009-07-15 |
Wilmer Ricciotti | Fixed dependency function, which was lacking the code... |
tree | commitdiff |
| 2009-07-15 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-07-15 |
Enrico Tassi | match_coercion gives back the saturations, not the... |
tree | commitdiff |
| 2009-07-14 |
denes | Fixed Option type error (OCaml bug) |
tree | commitdiff |
| 2009-07-14 |
denes | . |
tree | commitdiff |
| 2009-07-14 |
denes | . |
tree | commitdiff |
| 2009-07-13 |
Enrico Tassi | better spacing |
tree | commitdiff |
| 2009-07-13 |
Enrico Tassi | statistics are used, when possible, to sort |
tree | commitdiff |
| 2009-07-13 |
denes | Added statistics printings |
tree | commitdiff |
| 2009-07-13 |
denes | Added statistics module |
tree | commitdiff |
| 2009-07-13 |
Enrico Tassi | matitaprover is now flexible enough to allow the comput... |
tree | commitdiff |
| 2009-07-13 |
Claudio Sacerdoti... | Coercion hiding implemented. Notes: |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | initial implementation of coercion composition |
tree | commitdiff |
| 2009-07-10 |
denes | Removed unused parameter of unification procedure ... |
tree | commitdiff |
| 2009-07-10 |
Enrico Tassi | more profilers |
tree | commitdiff |
| 2009-07-10 |
Claudio Sacerdoti... | Bug fixed (missing ctx) + comment added. |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | initial implementation of `ncoercion name : type :... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | new nrepeat (and block '('...')' ) tactical |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | New functorialization: paramod is abstracted over a... |
tree | commitdiff |
| 2009-07-09 |
denes | Fixed check for condition iv p.33 (Riazzanov) |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | profile most operations, do not return a filtered varli... |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | 1 process for now |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | two cases should be assert false at least in TPTP |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | micro optimizations to unification |
tree | commitdiff |
| 2009-07-09 |
denes | Cleaned a bit |
tree | commitdiff |
| 2009-07-09 |
Enrico Tassi | ... |
tree | commitdiff |
| next |
projects / helm.git / history