]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_kernel
disambiguation now returns and takes in input the substitution
[helm.git] / helm / software / components / ng_kernel /
2008-10-27 Enrico Tassimetasenv passed to get_relevance, Metas that stand...
2008-10-27 Enrico Tassi_ in place of unused variables
2008-10-27 Enrico TassiImplicit annotationas are now printed
2008-10-21 Enrico Tassipsubst for metas fixed again
2008-10-20 Enrico Tassi...
2008-10-14 Enrico Tassimore work
2008-10-14 Enrico Tassiterm refinement almost done, some functions exported...
2008-10-13 Enrico Tassiinitial refiner ....
2008-10-13 Enrico Tassibug in psubst fixed inside local context in Irl form
2008-10-13 Enrico Tassibetter error message
2008-10-13 Enrico Tassippmetasenv & subst added
2008-10-13 Enrico TassiNCicReduction.reduce_machine returns a boolean stating...
2008-10-03 Enrico Tassi- NCicPp.ppterm applies the substitution
2008-10-03 Enrico Tassithe iterator was wrongly processing the application
2008-10-03 Wilmer RicciottiFinal implementation of proof irrelevant conversion...
2008-10-02 Enrico Tassi...
2008-10-02 Enrico Tassi...
2008-10-02 Enrico Tassiwe can test the unification algorithm!
2008-10-01 Enrico Tassicommented out unfinished code
2008-09-30 Enrico Tassi...
2008-09-30 Enrico Tassiunification completed
2008-09-25 Enrico Tassi...
2008-09-25 Enrico Tassi...
2008-09-24 Enrico Tassi...
2008-09-24 Enrico Tassi...
2008-09-24 Enrico Tassi...
2008-09-24 Enrico Tassi...
2008-09-24 Enrico Tassi...
2008-09-22 Enrico Tassinew iterator
2008-09-19 Enrico Tassimore comments and compare function for URI exported
2008-09-01 Claudio Sacerdoti... new debugging option
2008-08-21 Claudio Sacerdoti... Avoid warning.
2008-08-12 Wilmer RicciottiFixed two legacy comments
2008-08-01 Enrico Tassifixed recursiveness check
2008-07-30 Enrico Tassifixed allowed sort elim
2008-07-30 Claudio Sacerdoti... Missing check in positivity implemented: we did not...
2008-07-25 Enrico Tassi- too strict check on left parameters of constructors...
2008-07-23 Enrico Tassipositivity check fixed
2008-07-23 Enrico Tassi...
2008-07-23 Enrico Tassibetter ranking interface
2008-07-15 Enrico TassiCProp_i <= Type_i , Type_i <= CProp_i
2008-07-09 Enrico TassiCProp hierarchy fixed:
2008-06-13 Wilmer Ricciottifinal relevance check
2008-06-10 Wilmer Ricciottirelevance check for Match
2008-06-10 Wilmer RicciottiAdded check of relevance lists for inductive types...
2008-06-09 Wilmer RicciottiReverting to the previous version some files which...
2008-06-09 Wilmer Ricciottimore proof irrelevance
2008-06-04 Wilmer RicciottiProof-irrelevance check for all applications (first...
2008-06-04 Wilmer Ricciottiincomplete irrelevance test commented out
2008-05-30 Enrico Tassiirrelevance check half implemented but already impossib...
2008-05-30 Enrico Tassithanks to the fact that we convert well typed term...
2008-05-29 Enrico Tassirelevance check partially implemented but bugged since...
2008-05-29 Enrico Tassiunused variables removed
2008-05-29 Enrico Tassiref sync check fixed controlling fix/cofix coherence
2008-05-19 Claudio Sacerdoti... Here is where we should add relevance checks.
2008-05-19 Claudio Sacerdoti... Bug fixed in computation of leftnos: variables were...
2008-05-19 Claudio Sacerdoti... Code simplification.
2008-05-19 Claudio Sacerdoti... Added cprop <= type constraint.
2008-05-19 Claudio Sacerdoti... We do not need to give cprop a special status yet.
2008-05-19 Claudio Sacerdoti... ...
2008-05-19 Claudio Sacerdoti... CProp dropped in favour of a cprop universe exported...
2008-05-19 Enrico Tassiadded leftno to references f inductive types and constr...
2008-05-19 Enrico Tassiadded aps generation
2008-05-19 Enrico Tassi...
2008-05-19 Enrico Tassirenamed add_le_constraint to add_constraint since it...
2008-05-18 Claudio Sacerdoti... ...
2008-05-18 Claudio Sacerdoti... Bug fixed: when computing the left arguments, I was...
2008-05-18 Claudio Sacerdoti... New missing check implemented: the left parameters...
2008-05-18 Claudio Sacerdoti... Implemented translation of inductive types from the...
2008-05-18 Claudio Sacerdoti... Serious bug fixed: the max of two universes was compute...
2008-05-18 Claudio Sacerdoti... Synch with the paper.
2008-05-18 Claudio Sacerdoti... ...
2008-05-18 Claudio Sacerdoti... Error message improved.
2008-05-18 Claudio Sacerdoti... More effective optimization: avoid introducing already...
2008-05-17 Claudio Sacerdoti... New check implemented: the sort of each constructor...
2008-05-17 Claudio Sacerdoti... The file bug_universi.ma shows a strage case where...
2008-05-17 Claudio Sacerdoti... Missing whd.
2008-05-17 Claudio Sacerdoti... Bug fixed: since circular <= graphs are allowed, added...
2008-05-17 Claudio Sacerdoti... Bug fixed: only Type < Type1 was declared.
2008-05-17 Claudio Sacerdoti... Bug fixed and further code semplification in management...
2008-05-17 Claudio Sacerdoti... The code for universes was not correct in many borderli...
2008-05-16 Enrico Tassiadded new implementation of universes
2008-05-16 Enrico Tassiadded name_of_uri
2008-05-16 Enrico Tassimeta VS meta in alpha_eq honors substitution
2008-05-16 Enrico Tassiused ind/coind information in references
2008-05-16 Enrico Tassitypes where compared without lookig at test_eq_only
2008-05-15 Claudio Sacerdoti... Timings
2008-05-15 Enrico Tassi(Approximated) inference of relevance implemented:...
2008-05-15 Enrico TassiFirst implementation of irrelevance in conversion.
2008-05-15 Enrico TassiNew function get_relevance and new (not exported) funct...
2008-05-15 Enrico TassiBug fixed in computation of heights: a constant must...
2008-05-15 Enrico TassiImplementation of calculation of heights.
2008-05-15 Enrico TassiTypo fixed.
2008-05-15 Enrico TassiMajor code semplification and bugs removed (thanks...
2008-05-15 Andrea AspertiRemoved two args from psubst.
2008-05-15 Enrico Tassiheight of constants properly handled
2008-05-14 Claudio Sacerdoti... list_iter2_default_value moved to HExtlib. 1 euro to...
2008-05-14 Claudio Sacerdoti... eat_lambdas and eat_or_subst_lambdas taken out of the...
2008-05-14 Claudio Sacerdoti... debruijn simplified. It could go in nCicUtils, but...
2008-05-14 Claudio Sacerdoti... Bug fixed: types were check for conversion in the wrong...
next