2010-11-29 |
Claudio Sacerdoti... | Back-porting from new Matita: |
blob | commitdiff | raw |
2010-11-29 |
Claudio Sacerdoti... | Back-porting from new matita: |
blob | commitdiff | raw | diff to current |
2010-10-17 |
Enrico Tassi | new case for higher order unification: |
blob | commitdiff | raw | diff to current |
2010-09-30 |
Enrico Tassi | patches for hints & unification: |
blob | commitdiff | raw | diff to current |
2010-09-12 |
Enrico Tassi | Change (or better define) the order of hints premises. |
blob | commitdiff | raw | diff to current |
2010-07-22 |
Enrico Tassi | do not apply hints if metaclosed |
blob | commitdiff | raw | diff to current |
2010-05-06 |
Claudio Sacerdoti... | Bug fixed: |
blob | commitdiff | raw | diff to current |
2010-04-13 |
Enrico Tassi | catch the right exception, avoid uncaught Subst_not_found |
blob | commitdiff | raw | diff to current |
2010-03-01 |
Wilmer Ricciotti | Fixed a bug in the unification, which prevented some... |
blob | commitdiff | raw | diff to current |
2009-11-24 |
Wilmer Ricciotti | Bugfix in tipify: a metavariable was set to type withou... |
blob | commitdiff | raw | diff to current |
2009-11-24 |
Wilmer Ricciotti | When unifying |
blob | commitdiff | raw | diff to current |
2009-11-19 |
Wilmer Ricciotti | - Added a swap parameter to the unification procedure |
blob | commitdiff | raw | diff to current |
2009-11-04 |
Claudio Sacerdoti... | Bug fixed: restrict used to take the list of positions... |
blob | commitdiff | raw | diff to current |
2009-10-30 |
Claudio Sacerdoti... | Useless old code for ad-hoc management of out-scope... |
blob | commitdiff | raw | diff to current |
2009-10-29 |
Claudio Sacerdoti... | instantiate/sortfy/kindfy etc. reimplemented with less... |
blob | commitdiff | raw | diff to current |
2009-10-28 |
Claudio Sacerdoti... | Ad-hoc management of ? vs out_scope in instantiate... |
blob | commitdiff | raw | diff to current |
2009-10-28 |
Claudio Sacerdoti... | Commented out code to optimize the case t1 vs t2 when... |
blob | commitdiff | raw | diff to current |
2009-10-22 |
Enrico Tassi | new instantiate, only known bug is w.r.t. in/out scope... |
blob | commitdiff | raw | diff to current |
2009-10-16 |
Enrico Tassi | new lambda instros and better logging |
blob | commitdiff | raw | diff to current |
2009-10-15 |
Claudio Sacerdoti... | Profiling code integrated. |
blob | commitdiff | raw | diff to current |
2009-10-14 |
Enrico Tassi | hints were not used by reduction machines on heads |
blob | commitdiff | raw | diff to current |
2009-10-12 |
Claudio Sacerdoti... | 1) Bug fixed: the case Meta(i) vs Meta(i) was handled... |
blob | commitdiff | raw | diff to current |
2009-10-06 |
Enrico Tassi | unification pps can be activated by the menu debug |
blob | commitdiff | raw | diff to current |
2009-10-02 |
Enrico Tassi | hints input is cleared from projection redexes |
blob | commitdiff | raw | diff to current |
2009-10-01 |
Enrico Tassi | - delift_type_wrt_term fixed in many ways |
blob | commitdiff | raw | diff to current |
2009-10-01 |
Enrico Tassi | instantiate merges tags |
blob | commitdiff | raw | diff to current |
2009-10-01 |
Enrico Tassi | added sortification for (? args), untested code |
blob | commitdiff | raw | diff to current |
2009-10-01 |
Enrico Tassi | sortification simplified |
blob | commitdiff | raw | diff to current |
2009-09-30 |
Enrico Tassi | rewritten instantiate code |
blob | commitdiff | raw | diff to current |
2009-09-30 |
Claudio Sacerdoti... | New datatype for metasenv/subst: full fledged attribute... |
blob | commitdiff | raw | diff to current |
2009-09-30 |
Claudio Sacerdoti... | Better (but still broken) fix for the case ?sort vs... |
blob | commitdiff | raw | diff to current |
2009-09-29 |
Claudio Sacerdoti... | 1) improved (???) debugging, with |
blob | commitdiff | raw | diff to current |
2009-09-29 |
Claudio Sacerdoti... | The unification does not longer use the refiner (urrah!) |
blob | commitdiff | raw | diff to current |
2009-09-28 |
Enrico Tassi | better debug pp |
blob | commitdiff | raw | diff to current |
2009-09-21 |
Enrico Tassi | new implementation of delift_type_wrt_term, that call... |
blob | commitdiff | raw | diff to current |
2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
blob | commitdiff | raw | diff to current |
2009-09-15 |
Enrico Tassi | improved check in delift for flexible lc entries. |
blob | commitdiff | raw | diff to current |
2009-09-10 |
Enrico Tassi | to me, the problem: |
blob | commitdiff | raw | diff to current |
2009-09-04 |
Enrico Tassi | Reduction speedup (a.k.a. better sharing): |
blob | commitdiff | raw | diff to current |
2009-08-14 |
Claudio Sacerdoti... | Since the introduction of saturation, an assert false... |
blob | commitdiff | raw | diff to current |
2009-08-13 |
Claudio Sacerdoti... | fix_sorts (cfr. previous commit) used to break too... |
blob | commitdiff | raw | diff to current |
2009-08-13 |
Claudio Sacerdoti... | Let's refresh the universe to avoid assert failure. |
blob | commitdiff | raw | diff to current |
2009-07-30 |
Claudio Sacerdoti... | Don't reinvent the wheel. |
blob | commitdiff | raw | diff to current |
2009-07-24 |
Claudio Sacerdoti... | Beta-expansion was avoided as soon as one argument... |
blob | commitdiff | raw | diff to current |
2009-07-20 |
Claudio Sacerdoti... | Debugging printf removed |
blob | commitdiff | raw | diff to current |
2009-07-20 |
Claudio Sacerdoti... | Very serious bug fixed in unification, but the fix... |
blob | commitdiff | raw | diff to current |
2009-07-20 |
Claudio Sacerdoti... | 1) ppmetasenv and ppcontext to reduce the amount of... |
blob | commitdiff | raw | diff to current |
2009-06-17 |
Claudio Sacerdoti... | Initial implementation of statuses using objects in... |
blob | commitdiff | raw | diff to current |
2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status: |
blob | commitdiff | raw | diff to current |
2009-05-15 |
Claudio Sacerdoti... | Patch to add a debugging string to HExtlib.split_nth... |
blob | commitdiff | raw | diff to current |
2009-05-14 |
Ferruccio Guidi | - hExtlib: added debugging information for split_nth |
blob | commitdiff | raw | diff to current |
2009-05-11 |
Claudio Sacerdoti... | Bug fixed: the relevance list can be shorted then leftn... |
blob | commitdiff | raw | diff to current |
2009-04-29 |
Claudio Sacerdoti... | Refinement of inductive type implemented. |
blob | commitdiff | raw | diff to current |
2009-04-06 |
Claudio Sacerdoti... | New tactic clear; new syntax # _; to introduce and... |
blob | commitdiff | raw | diff to current |
2009-04-06 |
Enrico Tassi | tactic cases works! delift clears tags |
blob | commitdiff | raw | diff to current |
2009-04-06 |
Enrico Tassi | eta-contraction was made on the wrong term |
blob | commitdiff | raw | diff to current |
2009-04-06 |
Enrico Tassi | unification: |
blob | commitdiff | raw | diff to current |
2009-04-06 |
Enrico Tassi | snapshot |
blob | commitdiff | raw | diff to current |
2009-03-11 |
Enrico Tassi | unification hints with recursive calls do work! |
blob | commitdiff | raw | diff to current |
2009-03-10 |
Enrico Tassi | unificatiom hints with premises |
blob | commitdiff | raw | diff to current |
2009-03-10 |
Enrico Tassi | unification hints almost ready |
blob | commitdiff | raw | diff to current |
2009-03-03 |
Enrico Tassi | - fixed hint generation, more hints are generated |
blob | commitdiff | raw | diff to current |
2008-12-19 |
Enrico Tassi | added better debug_pps and add_user_provided_unificatio... |
blob | commitdiff | raw | diff to current |
2008-12-16 |
Enrico Tassi | hints attached |
blob | commitdiff | raw | diff to current |
2008-12-15 |
Wilmer Ricciotti | First attempt to implement unification hints. |
blob | commitdiff | raw | diff to current |
2008-12-11 |
Claudio Sacerdoti... | Applications are now processed from left to right. |
blob | commitdiff | raw | diff to current |
2008-12-05 |
Enrico Tassi | raise failure instead of uncertain if two terms are... |
blob | commitdiff | raw | diff to current |
2008-11-12 |
Enrico Tassi | more printings |
blob | commitdiff | raw | diff to current |
2008-11-06 |
Enrico Tassi | removed empty lines |
blob | commitdiff | raw | diff to current |
2008-10-27 |
Enrico Tassi | many bugs fixed |
blob | commitdiff | raw | diff to current |
2008-10-21 |
Enrico Tassi | - mk_restricted_irl removed, the non-optimized code... |
blob | commitdiff | raw | diff to current |
2008-10-20 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
2008-10-15 |
Enrico Tassi | subst_meta was missing |
blob | commitdiff | raw | diff to current |
2008-10-14 |
Enrico Tassi | more work |
blob | commitdiff | raw | diff to current |
2008-10-13 |
Enrico Tassi | NCicReduction.reduce_machine returns a boolean stating... |
blob | commitdiff | raw | diff to current |
2008-10-08 |
Wilmer Ricciotti | Fixed a performance problem with unif_machines and... |
blob | commitdiff | raw | diff to current |
2008-10-06 |
Enrico Tassi | slow example |
blob | commitdiff | raw | diff to current |
2008-10-06 |
Enrico Tassi | 3 nasty bugs fixed: |
blob | commitdiff | raw | diff to current |
2008-10-03 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
2008-10-03 |
Enrico Tassi | not so nice patch to small_delta_step |
blob | commitdiff | raw | diff to current |
2008-10-03 |
Enrico Tassi | - NCicPp.ppterm applies the substitution |
blob | commitdiff | raw | diff to current |
2008-10-03 |
Enrico Tassi | better debuggin output |
blob | commitdiff | raw | diff to current |
2008-10-02 |
Enrico Tassi | error... |
blob | commitdiff | raw | diff to current |
2008-10-02 |
Enrico Tassi | another divergence case patched |
blob | commitdiff | raw | diff to current |
2008-10-02 |
Enrico Tassi | to avoid a case of divergence small_delta_step checks... |
blob | commitdiff | raw | diff to current |
2008-09-30 |
Enrico Tassi | unification completed |
blob | commitdiff | raw | diff to current |
2008-09-29 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
2008-09-25 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
2008-09-25 |
Enrico Tassi | beta expand |
blob | commitdiff | raw | diff to current |
2008-09-25 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
2008-09-24 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
2008-09-24 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
2008-09-16 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
|