| 2010-11-29 |
Claudio Sacerdoti... | Bug fixed: propagation of left expected parameters... |
blob | commitdiff | raw |
| 2010-11-29 |
Claudio Sacerdoti... | In the case type_of constructor with expected type... |
blob | commitdiff | raw | diff to current |
| 2010-11-29 |
Claudio Sacerdoti... | Back-porting from new Matita: |
blob | commitdiff | raw | diff to current |
| 2010-06-17 |
Enrico Tassi | off by one fixed |
blob | commitdiff | raw | diff to current |
| 2010-06-08 |
Wilmer Ricciotti | Fixed a bug in the undebruijnate function which caused... |
blob | commitdiff | raw | diff to current |
| 2010-06-07 |
Enrico Tassi | unify left args of inductive types with left argus... |
blob | commitdiff | raw | diff to current |
| 2010-05-12 |
Wilmer Ricciotti | Experimental support for Russell (coercions moving... |
blob | commitdiff | raw | diff to current |
| 2009-11-24 |
Wilmer Ricciotti | In order to prevent useless meta extensions, we optimiz... |
blob | commitdiff | raw | diff to current |
| 2009-11-18 |
Wilmer Ricciotti | NCicRefiner.force_to_sort implemented on top of NCicUni... |
blob | commitdiff | raw | diff to current |
| 2009-11-18 |
Wilmer Ricciotti | Code factorization for check_type. |
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-29 |
Claudio Sacerdoti... | Better error message. |
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-14 |
Claudio Sacerdoti... | Debugging improved. |
blob | commitdiff | raw | diff to current |
| 2009-10-14 |
Claudio Sacerdoti... | Benchmarking integrated in folding/unfolding. |
blob | commitdiff | raw | diff to current |
| 2009-10-12 |
Claudio Sacerdoti... | Bug fixed: in case of (t ...) where t has flexible... |
blob | commitdiff | raw | diff to current |
| 2009-10-12 |
Claudio Sacerdoti... | Closed metas must have closed (expected) types. |
blob | commitdiff | raw | diff to current |
| 2009-10-12 |
Claudio Sacerdoti... | Improved debugging code. |
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-06 |
Claudio Sacerdoti... | Improved error message. |
blob | commitdiff | raw | diff to current |
| 2009-10-02 |
Claudio Sacerdoti... | Wrong context (again!) |
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-09-30 |
Claudio Sacerdoti... | New datatype for metasenv/subst: full fledged attribute... |
blob | commitdiff | raw | diff to current |
| 2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matit... |
blob | commitdiff | raw | diff to current |
| 2009-09-29 |
Claudio Sacerdoti... | Re-indentiation |
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 | - fixed bug in coercion application, input/output swapp... |
blob | commitdiff | raw | diff to current |
| 2009-09-21 |
Enrico Tassi | huge commit regarding universes: |
blob | commitdiff | raw | diff to current |
| 2009-09-16 |
Claudio Sacerdoti... | The left parameters coming from the constructor types... |
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-10 |
Enrico Tassi | the refiner was not checking that the resulting type |
blob | commitdiff | raw | diff to current |
| 2009-09-09 |
Enrico Tassi | some fixes here and there |
blob | commitdiff | raw | diff to current |
| 2009-09-09 |
Enrico Tassi | some more work for ng-coercions |
blob | commitdiff | raw | diff to current |
| 2009-09-08 |
Enrico Tassi | snapshot for CSC |
blob | commitdiff | raw | diff to current |
| 2009-07-31 |
Claudio Sacerdoti... | Bad patch reverted (in error message). |
blob | commitdiff | raw | diff to current |
| 2009-07-31 |
Claudio Sacerdoti... | Bug fixed: one case of too many arguments was not detec... |
blob | commitdiff | raw | diff to current |
| 2009-07-30 |
Claudio Sacerdoti... | First implementation of \ldots. |
blob | commitdiff | raw | diff to current |
| 2009-07-28 |
Claudio Sacerdoti... | 1) Some more work for vector implicits. |
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-08 |
Claudio Sacerdoti... | Improved error message. |
blob | commitdiff | raw | diff to current |
| 2009-07-08 |
Claudio Sacerdoti... | Bug fixed: the debrujinate function (hence the one... |
blob | commitdiff | raw | diff to current |
| 2009-06-18 |
Enrico Tassi | debug pps removed |
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-25 |
Enrico Tassi | nasty change in the lexer/parser: |
blob | commitdiff | raw | diff to current |
| 2009-05-18 |
Claudio Sacerdoti... | 1) order of processing of case branches reverted (to... |
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-10 |
Claudio Sacerdoti... | - critical bug fixed in NCicSubstitution.lift: |
blob | commitdiff | raw | diff to current |
| 2009-05-08 |
Claudio Sacerdoti... | Bug fixed: left parameters of constructors were unified... |
blob | commitdiff | raw | diff to current |
| 2009-05-08 |
Claudio Sacerdoti... | Bug fixed: refinement of mutual recursive definitions... |
blob | commitdiff | raw | diff to current |
| 2009-05-08 |
Claudio Sacerdoti... | Bug fixed in refinement of inductive types: left parame... |
blob | commitdiff | raw | diff to current |
| 2009-05-08 |
Claudio Sacerdoti... | The relevance list can be shorter than leftno (when... |
blob | commitdiff | raw | diff to current |
| 2009-05-05 |
Enrico Tassi | - pretty printer made robust in face of list_nth |
blob | commitdiff | raw | diff to current |
| 2009-04-29 |
Claudio Sacerdoti... | Refinement of inductive type implemented. |
blob | commitdiff | raw | diff to current |
| 2009-04-14 |
Claudio Sacerdoti... | Trick: the refiner always subst-expands the outtype... |
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 | snapshot |
blob | commitdiff | raw | diff to current |
| 2009-04-01 |
Enrico Tassi | 1) mk_meta now returns also the index of the created... |
blob | commitdiff | raw | diff to current |
| 2009-03-25 |
Enrico Tassi | new tactics are 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 |
| 2009-02-11 |
Enrico Tassi | some work to refine objs |
blob | commitdiff | raw | diff to current |
| 2008-12-19 |
Enrico Tassi | lambda case fixed, used to not properly use the expecte... |
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-12 |
Enrico Tassi | added some messages |
blob | commitdiff | raw | diff to current |
| 2008-12-09 |
Enrico Tassi | raise uncertain when a sort is not a sort but may be... |
blob | commitdiff | raw | diff to current |
| 2008-12-07 |
Claudio Sacerdoti... | Bug fixed: every time we form a Prod, we must typecheck... |
blob | commitdiff | raw | diff to current |
| 2008-12-05 |
Claudio Sacerdoti... | Debugging code removed |
blob | commitdiff | raw | diff to current |
| 2008-12-05 |
Enrico Tassi | a few missing ~subst added to whd |
blob | commitdiff | raw | diff to current |
| 2008-12-05 |
Enrico Tassi | coercions are there, but not heavily tested |
blob | commitdiff | raw | diff to current |
| 2008-12-04 |
Enrico Tassi | Fixes: |
blob | commitdiff | raw | diff to current |
| 2008-11-28 |
Enrico Tassi | it works! |
blob | commitdiff | raw | diff to current |
| 2008-11-28 |
Enrico Tassi | metas for terms have height 3 |
blob | commitdiff | raw | diff to current |
| 2008-11-06 |
Enrico Tassi | better error messages. sorts are compared using whd |
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 | some bug fixed |
blob | commitdiff | raw | diff to current |
| 2008-10-14 |
Enrico Tassi | more work |
blob | commitdiff | raw | diff to current |
| 2008-10-14 |
Enrico Tassi | term refinement almost done, some functions exported... |
blob | commitdiff | raw | diff to current |
| 2008-10-13 |
Enrico Tassi | initial refiner .... |
blob | commitdiff | raw | diff to current |
| 2008-09-16 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
|
projects / helm.git / history