]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_kernel
metavariable context has a separator now
[helm.git] / helm / software / components / ng_kernel /
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...
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... Generation of dot file.
2008-05-14 Claudio Sacerdoti... New licence used uniformly everywhere.
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-07 Claudio Sacerdoti... Update after some more bug fixing.
2008-05-07 Claudio Sacerdoti... Partially reverted bad merge by Enrico that re-introduc...
2008-05-05 Claudio Sacerdoti... More bugs fixed.
2008-05-05 Enrico Tassiget_check_fix and cofix unified, bug regarding debruijn...
2008-05-05 Enrico Tassiget_checked_indtys can take a constructor reference
2008-05-05 Enrico Tassiadded mk_cofix
2008-05-05 Enrico Tassilet corec
2008-05-05 Enrico TassiCoFix cache implemented
2008-05-05 Enrico Tassifix_left_in_constr still broken, ask enrico
2008-05-05 Enrico Tassiguarded_by_constructors implemented, some cleanup here...
2008-05-05 Enrico Tassiremoved dead code
2008-05-05 Enrico Tassi...
2008-05-03 Claudio Sacerdoti... Bug fixed in handling of explicit named substitutions...
2008-05-03 Claudio Sacerdoti... Broken XML files either fixed or removed.
2008-05-01 Claudio Sacerdoti... More precise classification of failures.
2008-05-01 Claudio Sacerdoti... List of all URIS comprising:
next