| 2009-10-07 |
Claudio Sacerdoti... | - oCic2NCic and nCic2OCic moved to ng_library |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | fixed constructor on non inductive type |
tree | commitdiff |
| 2009-10-06 |
Wilmer Ricciotti | Inverters/Inversion: |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | unification pps can be activated by the menu debug |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | ... |
tree | commitdiff |
| 2009-10-06 |
Enrico Tassi | nAuto W.I.P. |
tree | commitdiff |
| 2009-10-06 |
Claudio Sacerdoti... | Improved error message. |
tree | commitdiff |
| 2009-10-05 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | auto and auto_paramod are in nAuto |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | new file for auto |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | downcast removed |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | added auto_cache in the dupable status after an |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | new ng_library module |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | fixed bug in coercion application, input/output swapped... |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | if the query has a completely flexible side, the empty... |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | hints input is cleared from projection redexes |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | projections redex (proj (mk_foo ...)) where mk_foo |
tree | commitdiff |
| 2009-10-02 |
Wilmer Ricciotti | Updated command ninverter. Syntax: |
tree | commitdiff |
| 2009-10-02 |
Enrico Tassi | better nlet rec boxing |
tree | commitdiff |
| 2009-10-02 |
Claudio Sacerdoti... | Wrong context (again!) |
tree | commitdiff |
| 2009-10-02 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | - delift_type_wrt_term fixed in many ways |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | fixed the type of tactic_term, attributes were useless |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | instantiate merges tags |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | added sortification for (? args), untested code |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | sortification simplified |
tree | commitdiff |
| 2009-10-01 |
Enrico Tassi | fixed off-by-one |
tree | commitdiff |
| 2009-09-30 |
Enrico Tassi | rewritten instantiate code |
tree | commitdiff |
| 2009-09-30 |
Claudio Sacerdoti... | New datatype for metasenv/subst: full fledged attribute... |
tree | commitdiff |
| 2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matit... |
tree | commitdiff |
| 2009-09-30 |
Claudio Sacerdoti... | Better (but still broken) fix for the case ?sort vs... |
tree | commitdiff |
| 2009-09-30 |
Claudio Sacerdoti... | The term contains dummy.conv that was searched over... |
tree | commitdiff |
| 2009-09-29 |
Claudio Sacerdoti... | 1) improved (???) debugging, with |
tree | commitdiff |
| 2009-09-29 |
Claudio Sacerdoti... | Re-indentiation |
tree | commitdiff |
| 2009-09-29 |
Enrico Tassi | ugly coerc db print |
tree | commitdiff |
| 2009-09-29 |
Claudio Sacerdoti... | The unification does not longer use the refiner (urrah!) |
tree | commitdiff |
| 2009-09-28 |
Enrico Tassi | - fixed bug in coercion application, input/output swapp... |
tree | commitdiff |
| 2009-09-28 |
Enrico Tassi | 2 lift related bugs fixed! |
tree | commitdiff |
| 2009-09-28 |
Enrico Tassi | better debug pp |
tree | commitdiff |
| 2009-09-27 |
Enrico Tassi | Type printed as such, CProp printed as such |
tree | commitdiff |
| 2009-09-27 |
Enrico Tassi | fixpoint have attributes for pragma (i.e. they can... |
tree | commitdiff |
| 2009-09-23 |
Enrico Tassi | new macro screenshot |
tree | commitdiff |
| 2009-09-21 |
Enrico Tassi | new implementation of delift_type_wrt_term, that call... |
tree | commitdiff |
| 2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
tree | commitdiff |
| 2009-09-16 |
Claudio Sacerdoti... | The left parameters coming from the constructor types... |
tree | commitdiff |
| 2009-09-15 |
Enrico Tassi | improved check in delift for flexible lc entries. |
tree | commitdiff |
| 2009-09-14 |
Enrico Tassi | fixed coercion mechanism w.r.t. undo/require |
tree | commitdiff |
| 2009-09-14 |
Claudio Sacerdoti... | Slightly simplied status code. |
tree | commitdiff |
| 2009-09-14 |
Claudio Sacerdoti... | Simplest typing for status records. |
tree | commitdiff |
| 2009-09-14 |
Claudio Sacerdoti... | New tactics ncut and nlapply. |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | constructor accepts the arguments of the constructor... |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | new tactic constructor: @[n] |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | let rec/corec and co/inductive are not printed! |
tree | commitdiff |
| 2009-09-11 |
Enrico Tassi | new macro ncheck. fixed term2pres for Inductive and... |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | allow @{ ... } as the identifier of the letin |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | to me, the problem: |
tree | commitdiff |
| 2009-09-10 |
Enrico Tassi | the refiner was not checking that the resulting type |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | some fixes here and there |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | depends |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | some more work for ng-coercions |
tree | commitdiff |
| 2009-09-08 |
Enrico Tassi | snapshot for CSC |
tree | commitdiff |
| 2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing): |
tree | commitdiff |
| 2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing): |
tree | commitdiff |
| 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 |
| next |
projects / helm.git / history