| 2015-01-22 |
Ferruccio Guidi | dependences update |
tree | commitdiff |
| 2010-11-29 |
Claudio Sacerdoti... | Bug fixed: propagation of left expected parameters... |
tree | commitdiff |
| 2010-11-29 |
Claudio Sacerdoti... | In the case type_of constructor with expected type... |
tree | commitdiff |
| 2010-11-29 |
Claudio Sacerdoti... | Back-porting from new Matita: |
tree | commitdiff |
| 2010-11-29 |
Claudio Sacerdoti... | Back-porting from new Matita: |
tree | commitdiff |
| 2010-11-29 |
Claudio Sacerdoti... | Back-porting from new matita: |
tree | commitdiff |
| 2010-11-22 |
Claudio Sacerdoti... | Debugging code commented out. |
tree | commitdiff |
| 2010-10-17 |
Enrico Tassi | new case for higher order unification: |
tree | commitdiff |
| 2010-10-17 |
Enrico Tassi | removed wrong optimization in delift and export is_flexible |
tree | commitdiff |
| 2010-09-30 |
Enrico Tassi | patches for hints & unification: |
tree | commitdiff |
| 2010-09-12 |
Enrico Tassi | Change (or better define) the order of hints premises. |
tree | commitdiff |
| 2010-07-22 |
Enrico Tassi | do not apply hints if metaclosed |
tree | commitdiff |
| 2010-06-17 |
Enrico Tassi | off by one fixed |
tree | commitdiff |
| 2010-06-08 |
Wilmer Ricciotti | Fixed a bug in the undebruijnate function which caused... |
tree | commitdiff |
| 2010-06-07 |
Enrico Tassi | unify left args of inductive types with left argus... |
tree | commitdiff |
| 2010-05-12 |
Wilmer Ricciotti | Experimental support for Russell (coercions moving... |
tree | commitdiff |
| 2010-05-06 |
Claudio Sacerdoti... | Bug fixed: |
tree | commitdiff |
| 2010-04-13 |
Enrico Tassi | catch the right exception, avoid uncaught Subst_not_found |
tree | commitdiff |
| 2010-04-08 |
Claudio Sacerdoti... | New sets of. |
tree | commitdiff |
| 2010-03-24 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2010-03-04 |
Andrea Asperti | In line with the ml. |
tree | commitdiff |
| 2010-03-02 |
Enrico Tassi | Constants are indexed using the Reference, not the... |
tree | commitdiff |
| 2010-03-01 |
Wilmer Ricciotti | Fixed a bug in the unification, which prevented some... |
tree | commitdiff |
| 2009-11-24 |
Wilmer Ricciotti | Bugfix in tipify: a metavariable was set to type withou... |
tree | commitdiff |
| 2009-11-24 |
Wilmer Ricciotti | In order to prevent useless meta extensions, we optimiz... |
tree | commitdiff |
| 2009-11-24 |
Wilmer Ricciotti | When unifying |
tree | commitdiff |
| 2009-11-19 |
Wilmer Ricciotti | - Added a swap parameter to the unification procedure |
tree | commitdiff |
| 2009-11-18 |
Wilmer Ricciotti | NCicRefiner.force_to_sort implemented on top of NCicUni... |
tree | commitdiff |
| 2009-11-18 |
Wilmer Ricciotti | Code factorization for check_type. |
tree | commitdiff |
| 2009-11-16 |
Wilmer Ricciotti | Implementation of ndestruct tactic (including destructi... |
tree | commitdiff |
| 2009-11-04 |
Claudio Sacerdoti... | Bug fixed: restrict used to take the list of positions... |
tree | commitdiff |
| 2009-10-30 |
Claudio Sacerdoti... | Code simplified. |
tree | commitdiff |
| 2009-10-30 |
Claudio Sacerdoti... | Useless old code for ad-hoc management of out-scope... |
tree | commitdiff |
| 2009-10-30 |
Claudio Sacerdoti... | New style debugging/profiling for NCicMetaSubst. |
tree | commitdiff |
| 2009-10-29 |
Claudio Sacerdoti... | Better error message. |
tree | commitdiff |
| 2009-10-29 |
Claudio Sacerdoti... | instantiate/sortfy/kindfy etc. reimplemented with less... |
tree | commitdiff |
| 2009-10-29 |
Claudio Sacerdoti... | Let's use already existent functions. |
tree | commitdiff |
| 2009-10-28 |
Claudio Sacerdoti... | Ad-hoc management of ? vs out_scope in instantiate... |
tree | commitdiff |
| 2009-10-28 |
Claudio Sacerdoti... | Commented out code to optimize the case t1 vs t2 when... |
tree | commitdiff |
| 2009-10-22 |
Enrico Tassi | new instantiate, only known bug is w.r.t. in/out scope... |
tree | commitdiff |
| 2009-10-22 |
Enrico Tassi | the trie indexes terms up to 10 nested applications... |
tree | commitdiff |
| 2009-10-16 |
Enrico Tassi | new lambda instros and better logging |
tree | commitdiff |
| 2009-10-15 |
Claudio Sacerdoti... | Profiling code integrated. |
tree | commitdiff |
| 2009-10-14 |
Claudio Sacerdoti... | Debugging improved. |
tree | commitdiff |
| 2009-10-14 |
Claudio Sacerdoti... | Benchmarking integrated in folding/unfolding. |
tree | commitdiff |
| 2009-10-14 |
Enrico Tassi | hints were not used by reduction machines on heads |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | 1) Bug fixed: the case Meta(i) vs Meta(i) was handled... |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | Bug fixed: in case of (t ...) where t has flexible... |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | Closed metas must have closed (expected) types. |
tree | commitdiff |
| 2009-10-12 |
Claudio Sacerdoti... | Improved debugging code. |
tree | commitdiff |
| 2009-10-07 |
Claudio Sacerdoti... | - oCic2NCic and nCic2OCic moved to ng_library |
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 |
Claudio Sacerdoti... | Improved error message. |
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 | 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 |
Wilmer Ricciotti | Updated command ninverter. Syntax: |
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 | 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-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-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 |
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-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-08-14 |
Claudio Sacerdoti... | Since the introduction of saturation, an assert false... |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | fix_sorts (cfr. previous commit) used to break too... |
tree | commitdiff |
| 2009-08-13 |
Claudio Sacerdoti... | Let's refresh the universe to avoid assert failure. |
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-30 |
Claudio Sacerdoti... | First implementation of \ldots. |
tree | commitdiff |
| 2009-07-30 |
Claudio Sacerdoti... | Don't reinvent the wheel. |
tree | commitdiff |
| 2009-07-28 |
Claudio Sacerdoti... | 1) Some more work for vector implicits. |
tree | commitdiff |
| 2009-07-27 |
Claudio Sacerdoti... | Stupid bug fixed: the test to detect Uncertain cases... |
tree | commitdiff |
| next |
projects / helm.git / history