]> matita.cs.unibo.it Git - helm.git/shortlog
helm.git
2008-05-19 Enrico Tassiadded leftno to references f inductive types and constr...
2008-05-19 Enrico Tassiadded aps generation
2008-05-19 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
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... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Enrico Tassirun fsub during night
2008-05-18 Claudio Sacerdoti... Bug fixed: when computing the left arguments, I was...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Enrico Tassinames fixed accoding to the new ones generated after...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Enrico Tassirevert last commit, context' -> context (added comment)
2008-05-18 Enrico Tassiusing the right names in the context to check match...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... New missing check implemented: the left parameters...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent types are no longer cleaned in inductiv...
2008-05-18 Claudio Sacerdoti... Dummy dependent products in inductive types arities...
2008-05-18 Claudio Sacerdoti... This commit avoids cleaning dummy dependent types in...
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 Enrico Tassiimpredicative Set is considered as Prop in the new...
2008-05-17 Claudio Sacerdoti... New check implemented: the sort of each constructor...
2008-05-17 Claudio Sacerdoti... Missing 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 Tassiranking reports the lest of univs
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 TassiNew function list_forall_default3. 3 euros to the first...
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...
2008-05-14 Claudio Sacerdoti... We forgot an important check: the declared and expected...
2008-05-14 Enrico Tassipartial implementation of reduction up to a given height
2008-05-14 Enrico Tassifixed error message
2008-05-14 Claudio Sacerdoti... New checks for well-formedness of metasenvs and substs.
2008-05-14 Claudio Sacerdoti... nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_...
2008-05-14 Claudio Sacerdoti... Nicer graph.
2008-05-14 Claudio Sacerdoti... map_hash moved to HExtlib
2008-05-14 Claudio Sacerdoti... New function map_hash.
2008-05-14 Claudio Sacerdoti... Generation of dot file.
2008-05-14 Claudio Sacerdoti... New licence used uniformly everywhere.
2008-05-13 Ferruccio Guidiwe added a link to lambda-delta home page in the hope...
2008-05-13 Claudio Sacerdoti... One more bug fixed: we tried to perform List.nth on...
2008-05-13 Claudio Sacerdoti... More exceptions captured.
2008-05-13 Claudio Sacerdoti... Bug fixed in pretty-printing of free Rels.
2008-05-13 Claudio Sacerdoti... Never commit before trying to compile... stupid typo...
2008-05-13 Claudio Sacerdoti... Used old kernel exception in place of brand new one.
2008-05-13 Claudio Sacerdoti... - is_closed removed from the kernel (it used to make...
2008-05-13 Claudio Sacerdoti... Library factorized out.
2008-05-13 Enrico Tassiwrong test equality only fixed
2008-05-13 Claudio Sacerdoti... Type of conjecture and subst_entry made uniform.
2008-05-13 Enrico Tassiconvertibility was taking a metasenv but not using it
2008-05-13 Claudio Sacerdoti... Added boolean "is_inductive" to NReference.Ind
2008-05-12 Claudio Sacerdoti... trust is always false by default
2008-05-12 Claudio Sacerdoti... trust implemented, but in the nCicTypeChecker!
2008-05-12 Claudio Sacerdoti... New implementation of CicEnvironment:
2008-05-12 Enrico Tassiheight is stored in the reference, no need to fetch...
2008-05-10 Enrico Tassifixed english
2008-05-10 Enrico Tassivalid xml
2008-05-10 Enrico Tassi...
2008-05-10 Enrico Tassi...
2008-05-10 Enrico Tassireleased 0.5.0
2008-05-10 Enrico Tassi...
2008-05-10 Enrico Tassi...
2008-05-10 Enrico Tassisome files orphaned
2008-05-09 Enrico Tassi...
2008-05-09 Enrico Tassia missing prime
2008-05-09 Claudio Sacerdoti... Bug fixed: the domain of a LetRec was only made by...
next