]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_kernel
Cic.term and Cic.obj unused!
[helm.git] / helm / software / components / ng_kernel /
2009-04-29 Claudio Sacerdoti... Refinement of inductive type implemented.
2009-04-26 Claudio Sacerdoti... The backward compatible management of aliases for NG...
2009-04-25 Claudio Sacerdoti... Lookup_in_library implemented for new objects. Basicall...
2009-04-25 Claudio Sacerdoti... Better error message.
2009-04-24 Claudio Sacerdoti... Quick&dirty implementation of neqd:
2009-04-14 Ferruccio Guidiwe rebuilt the dependences
2009-04-10 Claudio Sacerdoti... The sequent viewer now considers the context to render...
2009-04-06 Claudio Sacerdoti... New tactic clear; new syntax # _; to introduce and...
2009-04-06 Enrico Tassibetter error message
2009-04-01 Enrico Tassiadded tentative elim
2009-04-01 Enrico Tassiremoved spurious "
2009-03-25 Enrico Tassinew tactics are almost ready
2009-03-11 Ferruccio Guidinew dependences
2009-03-11 Enrico Tassiadded margin option to the pp
2009-03-03 Enrico Tassi- fixed hint generation, more hints are generated
2009-02-17 Ferruccio Guidi- Coq/preamble: missing alias added
2009-02-11 Enrico Tassisome work to refine objs
2009-01-30 Enrico Tassifix convertibility in case of application test_eq_only...
2008-12-19 Enrico Tassibetter pps
2008-12-19 Enrico Tassihandles bad Appl
2008-12-16 Enrico Tassiprevious change was causing divergence
2008-12-16 Enrico Tassifixed a bug, it used to report o wrong is_normal bit...
2008-12-16 Enrico Tassiwrap object_not_found
2008-12-12 Enrico Tassibetter error message, functions to clear various caches...
2008-12-09 Enrico Tassibetter max function (instead of @) for combining universes
2008-12-05 Enrico Tassia few missing ~subst added to whd
2008-12-05 Enrico Tassicoercions are there, but not heavily tested
2008-12-04 Enrico TassiFixes:
2008-11-28 Enrico Tassinew disambiguator almost attached
2008-11-27 Enrico Tassi1. grafiteDisambiguator => multiPassDisambiguator
2008-11-21 Enrico Tassiloc * lazy string -> (loc * string) lazy
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...
next