| 2015-01-22 |
Ferruccio Guidi | dependences update |
tree | commitdiff |
| 2010-03-24 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-11-16 |
Wilmer Ricciotti | Implementation of ndestruct tactic (including destructi... |
tree | commitdiff |
| 2009-10-06 |
Wilmer Ricciotti | Inverters/Inversion: |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | added auto_cache in the dupable status after an |
tree | commitdiff |
| 2009-10-02 |
Wilmer Ricciotti | Updated command ninverter. Syntax: |
tree | commitdiff |
| 2009-10-02 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matit... |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | depends |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | some more work for ng-coercions |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
tree | commitdiff |
| 2009-06-25 |
Ferruccio Guidi | - some depend files :) |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status: |
tree | commitdiff |
| 2009-06-09 |
Claudio Sacerdoti... | Debugging code removed. |
tree | commitdiff |
| 2009-06-09 |
Claudio Sacerdoti... | Temporary (and partially broken) patch for Ferruccio... |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | nothing special |
tree | commitdiff |
| 2009-05-15 |
Claudio Sacerdoti... | Patch to add a debugging string to HExtlib.split_nth... |
tree | commitdiff |
| 2009-05-14 |
Ferruccio Guidi | - hExtlib: added debugging information for split_nth |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-04-28 |
Enrico Tassi | huge commit in automation: |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | we rebuilt the dependences |
tree | commitdiff |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
| 2009-01-26 |
Enrico Tassi | added a number to identical error messages to ease... |
tree | commitdiff |
| 2009-01-19 |
Enrico Tassi | all pullbacks are attempted in sequence, removed many... |
tree | commitdiff |
| 2009-01-16 |
Enrico Tassi | ceommented out metasenv |
tree | commitdiff |
| 2009-01-15 |
Enrico Tassi | unvariant also for coercions to funclass |
tree | commitdiff |
| 2009-01-15 |
Enrico Tassi | coercions that are marked as variant are unfolded when... |
tree | commitdiff |
| 2009-01-15 |
Enrico Tassi | Coercions graph is printed between real types and not... |
tree | commitdiff |
| 2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
tree | commitdiff |
| 2009-01-08 |
Enrico Tassi | more composites to make all happy! |
tree | commitdiff |
| 2008-12-24 |
Enrico Tassi | bug fixed, all convertible was called without a metasenv |
tree | commitdiff |
| 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 |
| next |
projects / helm.git / history