| 2008-12-19 |
Enrico Tassi | identity coercions are not really inserted, just used... |
tree | commitdiff |
| 2008-12-18 |
Claudio Sacerdoti... | Stupid bug fixed: checkin the type in place of the... |
tree | commitdiff |
| 2008-12-18 |
Claudio Sacerdoti... | Now it compiles again. |
tree | commitdiff |
| 2008-12-18 |
Claudio Sacerdoti... | Refinement of axioms fixed. We did not check that the... |
tree | commitdiff |
| 2008-12-15 |
Enrico Tassi | To check if a term is type, do a whd of its sort before... |
tree | commitdiff |
| 2008-11-28 |
Ferruccio Guidi | ng_disambiguation ng_kernel ng_refiner disambiguation... |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | missing subst added, now apply rule is probably enough... |
tree | commitdiff |
| 2008-11-15 |
Enrico Tassi | disambiguation can use a goal as hint for the expected... |
tree | commitdiff |
| 2008-10-14 |
Enrico Tassi | term refinement almost done, some functions exported... |
tree | commitdiff |
| 2008-09-18 |
Claudio Sacerdoti... | ppterm_in_named_context removed in favour of the high... |
tree | commitdiff |
| 2008-09-18 |
Claudio Sacerdoti... | In case of coercion to Prod, the error message shown... |
tree | commitdiff |
| 2008-09-08 |
Claudio Sacerdoti... | Case c1 t1 vs c2 t2 where c1 and c2 are not splitted... |
tree | commitdiff |
| 2008-09-05 |
Enrico Tassi | unification+pullback fix. It used to saturate a coercio... |
tree | commitdiff |
| 2008-09-04 |
Enrico Tassi | fixed case of divergence |
tree | commitdiff |
| 2008-08-21 |
Claudio Sacerdoti... | Added catching of an exception to implement a missing... |
tree | commitdiff |
| 2008-07-15 |
Enrico Tassi | CProp_i <= Type_i , Type_i <= CProp_i |
tree | commitdiff |
| 2008-07-10 |
Enrico Tassi | fixed regression in casting an argument to funclass... |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
tree | commitdiff |
| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info... |
tree | commitdiff |
| 2008-06-13 |
Enrico Tassi | replace assert false with AssertFailure |
tree | commitdiff |
| 2008-06-11 |
Enrico Tassi | meta not considered before in outtype |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | prod moved under lambda-prolog unification case |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | added a bit more reduction in case Prod v.s. term,... |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | the type of the match was obtained reducing the outtype |
tree | commitdiff |
| 2008-05-18 |
Enrico Tassi | using the right names in the context to check match... |
tree | commitdiff |
| 2008-05-18 |
Claudio Sacerdoti... | This commit avoids cleaning dummy dependent types in... |
tree | commitdiff |
| 2008-04-22 |
Enrico Tassi | oblivion ugraph everywhere outside the kernel |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | new calculation of recursive parameters in guarded... |
tree | commitdiff |
| 2008-03-12 |
Claudio Sacerdoti... | Almost always correct optimization: during unification... |
tree | commitdiff |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | check_metasenv_consistency: |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Potentially (and, at least sometimes, actually) big... |
tree | commitdiff |
| 2007-12-04 |
Claudio Sacerdoti... | Even if the error is not localized, it was not a good... |
tree | commitdiff |
| 2007-12-04 |
Claudio Sacerdoti... | Some terms are not localized from the very beginning :-( |
tree | commitdiff |
| 2007-12-04 |
Claudio Sacerdoti... | One more error localized. But the code is really ugly... |
tree | commitdiff |
| 2007-11-28 |
Claudio Sacerdoti... | Bug fixed: an unification exception used to escape... |
tree | commitdiff |
| 2007-11-25 |
Claudio Sacerdoti... | Bug fixed: an unification exception used to escape... |
tree | commitdiff |
| 2007-11-23 |
Enrico Tassi | restored the right context used to generate names.... |
tree | commitdiff |
| 2007-11-15 |
Enrico Tassi | removed ugly prerr_endline |
tree | commitdiff |
| 2007-11-15 |
Enrico Tassi | added ~delta parameter to saturate_term and used it... |
tree | commitdiff |
| 2007-10-26 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: a MutCase considering a wrong number of... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Recently introduced bug fixed: error localization was... |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-09-19 |
Enrico Tassi | commented out pack coercion, since the code is not... |
tree | commitdiff |
| 2007-09-09 |
Enrico Tassi | in the case of coerce_to_sort the whd was done with... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | huge commit regarding coercions to funclass and eat_pro... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | 1. fix_arity fixed: the code is totally wrong and this... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | when a coercion is passed through a case on right-param... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | ooops, missing ) |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | fixed propagation under Fix/Lambda/Case of coercions... |
tree | commitdiff |
| 2007-09-06 |
Enrico Tassi | coercions under Fix and Case. Code refactoring needed |
tree | commitdiff |
| 2007-09-06 |
Enrico Tassi | added a duplicated implementation of replace lifting |
tree | commitdiff |
| 2007-09-05 |
Claudio Sacerdoti... | coercions are propagated under Fix (but not mutually... |
tree | commitdiff |
| 2007-08-31 |
Enrico Tassi | fixed coercions between arrows when the arrow is dependent. |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | captured exception preserved (was replaced blindly... |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | refactoring of all coercions code and add a check to... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | Coercions rework: |
tree | commitdiff |
| 2007-08-22 |
Claudio Sacerdoti... | Avoid reusing Hbeta several times. |
tree | commitdiff |
| 2007-07-19 |
Enrico Tassi | COERCIONS: tentative addition of an equivalence relatio... |
tree | commitdiff |
| 2007-06-23 |
Enrico Tassi | removed ugly printings |
tree | commitdiff |
| 2007-05-22 |
Claudio Sacerdoti... | Slightly more efficient patch. |
tree | commitdiff |
| 2007-05-07 |
Enrico Tassi | a bit of sharing and the optimization of not folding... |
tree | commitdiff |
| 2007-04-24 |
Andrea Asperti | @ |
tree | commitdiff |
| 2007-04-12 |
Enrico Tassi | HACK for indtype checking |
tree | commitdiff |
| 2007-04-05 |
Enrico Tassi | many printings added |
tree | commitdiff |
| 2007-02-08 |
Claudio Sacerdoti... | Important commit: |
tree | commitdiff |
| 2007-02-02 |
Claudio Sacerdoti... | Serious bug fixed: the types of a real mutual fix defin... |
tree | commitdiff |
| 2007-01-30 |
Claudio Sacerdoti... | Behaviour of CicRefine.type_of_aux' on MutCases changed... |
tree | commitdiff |
| 2007-01-05 |
Enrico Tassi | Added check for duplicate (convertible) composite coerc... |
tree | commitdiff |
| 2007-01-02 |
Claudio Sacerdoti... | Same fix of the previous commit, but in a different... |
tree | commitdiff |
| 2007-01-02 |
Claudio Sacerdoti... | 1. More debugging code |
tree | commitdiff |
| 2007-01-02 |
Enrico Tassi | added oblivion_universe and used it in paxck_coercions |
tree | commitdiff |
| 2006-12-29 |
Ferruccio Guidi | now we try two distinct depend files for compilation... |
tree | commitdiff |
| 2006-12-28 |
Claudio Sacerdoti... | Yet another localization error in eat_prods fixed. |
tree | commitdiff |
| 2006-12-14 |
Enrico Tassi | ... |
tree | commitdiff |
| 2006-12-14 |
Claudio Sacerdoti... | Huge commit: |
tree | commitdiff |
| 2006-11-25 |
Enrico Tassi | added assertion (that is a TODO) in case non-considered... |
tree | commitdiff |
| 2006-11-12 |
Claudio Sacerdoti... | The pretty printers in CicPp now have an optional ... |
tree | commitdiff |
| 2006-10-28 |
Claudio Sacerdoti... | GRAVE BUG IN COERCIONS FIXED: the insertion of a coerci... |
tree | commitdiff |
| 2006-10-25 |
Claudio Sacerdoti... | 1. is_meta_closed should be applied only to terms on... |
tree | commitdiff |
| 2006-10-23 |
Claudio Sacerdoti... | Better (and more localized) error message for sort_of_prod. |
tree | commitdiff |
| 2006-10-23 |
Claudio Sacerdoti... | CicUniv.UniverseInconsistency is no handled correcly. |
tree | commitdiff |
| 2006-10-20 |
Andrea Asperti | The function exists_a_meta has been modified to capture... |
tree | commitdiff |
| 2006-10-20 |
Andrea Asperti | New function pack_coercion_metasenv, used in auto after... |
tree | commitdiff |
| 2006-10-19 |
Claudio Sacerdoti... | Bug fixed: when trying to insert coercions after an... |
tree | commitdiff |
| 2006-10-19 |
Claudio Sacerdoti... | Potential performance improvement + better disambiguati... |
tree | commitdiff |
| 2006-10-18 |
Claudio Sacerdoti... | Too verbose error message (probably activated by Enrico... |
tree | commitdiff |
| 2006-10-09 |
Claudio Sacerdoti... | Bugs fixed in merging of composite coercions. In partic... |
tree | commitdiff |
| 2006-10-09 |
Claudio Sacerdoti... | Comments updated with new reflections. |
tree | commitdiff |
| 2006-10-06 |
Claudio Sacerdoti... | 1. some "try ... with _ " removed |
tree | commitdiff |
| 2006-09-27 |
Claudio Sacerdoti... | More informative error message. |
tree | commitdiff |
| 2006-09-15 |
Claudio Sacerdoti... | Yet another refinement error localized. |
tree | commitdiff |
| 2006-09-15 |
Claudio Sacerdoti... | Debugging code deactivated. |
tree | commitdiff |
| 2006-09-05 |
Enrico Tassi | fixed coercions. composite can't occur if to funclass |
tree | commitdiff |
| 2006-09-04 |
Enrico Tassi | BIG FAT COMMIT REGARDING COERCIONS: |
tree | commitdiff |
| 2006-07-26 |
Claudio Sacerdoti... | Patch to the unification to make the case (i l) vs... |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | Unification improved to handle beta-delta conversion... |
tree | commitdiff |
| next |
projects / helm.git / history