]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/cic_unification
\ldots are now used in nelim and ncases
[helm.git] / helm / software / components / cic_unification /
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces...
2009-06-25 Ferruccio Guidi- some depend files :)
2009-06-15 Enrico Tassihuge commit regarding the grafite_status:
2009-06-09 Claudio Sacerdoti... Debugging code removed.
2009-06-09 Claudio Sacerdoti... Temporary (and partially broken) patch for Ferruccio...
2009-05-18 Enrico Tassinothing special
2009-05-15 Claudio Sacerdoti... Patch to add a debugging string to HExtlib.split_nth...
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth
2009-05-08 Claudio Sacerdoti... ...
2009-04-28 Enrico Tassihuge commit in automation:
2009-04-14 Ferruccio Guidiwe rebuilt the dependences
2009-03-25 Enrico Tassinew tactics are almost ready
2009-01-26 Enrico Tassiadded a number to identical error messages to ease...
2009-01-19 Enrico Tassiall pullbacks are attempted in sequence, removed many...
2009-01-16 Enrico Tassiceommented out metasenv
2009-01-15 Enrico Tassiunvariant also for coercions to funclass
2009-01-15 Enrico Tassicoercions that are marked as variant are unfolded when...
2009-01-15 Enrico TassiCoercions graph is printed between real types and not...
2009-01-13 Enrico Tassimany changes regarding coercions:
2009-01-08 Enrico Tassimore composites to make all happy!
2008-12-24 Enrico Tassibug fixed, all convertible was called without a metasenv
2008-12-19 Enrico Tassiidentity coercions are not really inserted, just used...
2008-12-18 Claudio Sacerdoti... Stupid bug fixed: checkin the type in place of the...
2008-12-18 Claudio Sacerdoti... Now it compiles again.
2008-12-18 Claudio Sacerdoti... Refinement of axioms fixed. We did not check that the...
2008-12-15 Enrico TassiTo check if a term is type, do a whd of its sort before...
2008-11-28 Ferruccio Guiding_disambiguation ng_kernel ng_refiner disambiguation...
2008-11-15 Enrico Tassimissing subst added, now apply rule is probably enough...
2008-11-15 Enrico Tassidisambiguation can use a goal as hint for the expected...
2008-10-14 Enrico Tassiterm refinement almost done, some functions exported...
2008-09-18 Claudio Sacerdoti... ppterm_in_named_context removed in favour of the high...
2008-09-18 Claudio Sacerdoti... In case of coercion to Prod, the error message shown...
2008-09-08 Claudio Sacerdoti... Case c1 t1 vs c2 t2 where c1 and c2 are not splitted...
2008-09-05 Enrico Tassiunification+pullback fix. It used to saturate a coercio...
2008-09-04 Enrico Tassifixed case of divergence
2008-08-21 Claudio Sacerdoti... Added catching of an exception to implement a missing...
2008-07-15 Enrico TassiCProp_i <= Type_i , Type_i <= CProp_i
2008-07-10 Enrico Tassifixed regression in casting an argument to funclass...
2008-07-09 Enrico TassiCProp hierarchy fixed:
2008-07-07 Enrico Tassisimplified coercDb implementation with additional info...
2008-06-13 Enrico Tassireplace assert false with AssertFailure
2008-06-11 Enrico Tassimeta not considered before in outtype
2008-05-30 Enrico TassiCProp hierarchy is there!
2008-05-30 Enrico Tassiprod moved under lambda-prolog unification case
2008-05-30 Enrico Tassiadded a bit more reduction in case Prod v.s. term,...
2008-05-29 Enrico Tassithe type of the match was obtained reducing the outtype
2008-05-18 Enrico Tassiusing the right names in the context to check match...
2008-05-18 Claudio Sacerdoti... This commit avoids cleaning dummy dependent types in...
2008-04-22 Enrico Tassioblivion ugraph everywhere outside the kernel
2008-04-17 Enrico Tassinew calculation of recursive parameters in guarded...
2008-03-12 Claudio Sacerdoti... Almost always correct optimization: during unification...
2008-03-11 Claudio Sacerdoti... Very experimental commit: the type of the source is...
2008-03-10 Claudio Sacerdoti... check_metasenv_consistency:
2008-03-09 Claudio Sacerdoti... Potentially (and, at least sometimes, actually) big...
2007-12-04 Claudio Sacerdoti... Even if the error is not localized, it was not a good...
2007-12-04 Claudio Sacerdoti... Some terms are not localized from the very beginning :-(
2007-12-04 Claudio Sacerdoti... One more error localized. But the code is really ugly...
2007-11-28 Claudio Sacerdoti... Bug fixed: an unification exception used to escape...
2007-11-25 Claudio Sacerdoti... Bug fixed: an unification exception used to escape...
2007-11-23 Enrico Tassirestored the right context used to generate names....
2007-11-15 Enrico Tassiremoved ugly prerr_endline
2007-11-15 Enrico Tassiadded ~delta parameter to saturate_term and used it...
2007-10-26 Enrico Tassi...
2007-10-25 Claudio Sacerdoti... Bug fixed: a MutCase considering a wrong number of...
2007-10-25 Claudio Sacerdoti... Recently introduced bug fixed: error localization was...
2007-10-12 Claudio Sacerdoti... Move to OCaml 3.10. Requires debian packages from unsta...
2007-09-19 Enrico Tassicommented out pack coercion, since the code is not...
2007-09-09 Enrico Tassiin the case of coerce_to_sort the whd was done with...
2007-09-08 Enrico Tassihuge commit regarding coercions to funclass and eat_pro...
2007-09-07 Enrico Tassi1. fix_arity fixed: the code is totally wrong and this...
2007-09-07 Enrico Tassiwhen a coercion is passed through a case on right-param...
2007-09-07 Enrico Tassiooops, missing )
2007-09-07 Enrico Tassifixed propagation under Fix/Lambda/Case of coercions...
2007-09-06 Enrico Tassicoercions under Fix and Case. Code refactoring needed
2007-09-06 Enrico Tassiadded a duplicated implementation of replace lifting
2007-09-05 Claudio Sacerdoti... coercions are propagated under Fix (but not mutually...
2007-08-31 Enrico Tassifixed coercions between arrows when the arrow is dependent.
2007-08-30 Enrico Tassicaptured exception preserved (was replaced blindly...
2007-08-30 Enrico Tassirefactoring of all coercions code and add a check to...
2007-08-30 Claudio Sacerdoti... Coercions are now generalized to the general form
2007-08-30 Enrico TassiCoercions rework:
2007-08-22 Claudio Sacerdoti... Avoid reusing Hbeta several times.
2007-07-19 Enrico TassiCOERCIONS: tentative addition of an equivalence relatio...
2007-06-23 Enrico Tassiremoved ugly printings
2007-05-22 Claudio Sacerdoti... Slightly more efficient patch.
2007-05-07 Enrico Tassia bit of sharing and the optimization of not folding...
2007-04-24 Andrea Asperti@
2007-04-12 Enrico TassiHACK for indtype checking
2007-04-05 Enrico Tassimany printings added
2007-02-08 Claudio Sacerdoti... Important commit:
2007-02-02 Claudio Sacerdoti... Serious bug fixed: the types of a real mutual fix defin...
2007-01-30 Claudio Sacerdoti... Behaviour of CicRefine.type_of_aux' on MutCases changed...
2007-01-05 Enrico TassiAdded check for duplicate (convertible) composite coerc...
2007-01-02 Claudio Sacerdoti... Same fix of the previous commit, but in a different...
2007-01-02 Claudio Sacerdoti... 1. More debugging code
2007-01-02 Enrico Tassiadded oblivion_universe and used it in paxck_coercions
2006-12-29 Ferruccio Guidinow we try two distinct depend files for compilation...
2006-12-28 Claudio Sacerdoti... Yet another localization error in eat_prods fixed.
2006-12-14 Enrico Tassi...
2006-12-14 Claudio Sacerdoti... Huge commit:
next