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