]> 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
- Procedural: generation of "exact" is now complete
[helm.git] / helm / software / components / ng_kernel /
2009-04-10 Claudio Sacerdoti... The sequent viewer now considers the context to render... tree | commitdiff
2009-04-06 Claudio Sacerdoti... New tactic clear; new syntax # _; to introduce and... tree | commitdiff
2009-04-06 Enrico Tassibetter error message tree | commitdiff
2009-04-01 Enrico Tassiadded tentative elim tree | commitdiff
2009-04-01 Enrico Tassiremoved spurious " tree | commitdiff
2009-03-25 Enrico Tassinew tactics are almost ready tree | commitdiff
2009-03-11 Ferruccio Guidinew dependences tree | commitdiff
2009-03-11 Enrico Tassiadded margin option to the pp tree | commitdiff
2009-03-03 Enrico Tassi- fixed hint generation, more hints are generated tree | commitdiff
2009-02-17 Ferruccio Guidi- Coq/preamble: missing alias added tree | commitdiff
2009-02-11 Enrico Tassisome work to refine objs tree | commitdiff
2009-01-30 Enrico Tassifix convertibility in case of application test_eq_only... tree | commitdiff
2008-12-19 Enrico Tassibetter pps tree | commitdiff
2008-12-19 Enrico Tassihandles bad Appl tree | commitdiff
2008-12-16 Enrico Tassiprevious change was causing divergence tree | commitdiff
2008-12-16 Enrico Tassifixed a bug, it used to report o wrong is_normal bit... tree | commitdiff
2008-12-16 Enrico Tassiwrap object_not_found tree | commitdiff
2008-12-12 Enrico Tassibetter error message, functions to clear various caches... tree | commitdiff
2008-12-09 Enrico Tassibetter max function (instead of @) for combining universes tree | commitdiff
2008-12-05 Enrico Tassia few missing ~subst added to whd tree | commitdiff
2008-12-05 Enrico Tassicoercions are there, but not heavily tested tree | commitdiff
2008-12-04 Enrico TassiFixes: tree | commitdiff
2008-11-28 Enrico Tassinew disambiguator almost attached tree | commitdiff
2008-11-27 Enrico Tassi1. grafiteDisambiguator => multiPassDisambiguator tree | commitdiff
2008-11-21 Enrico Tassiloc * lazy string -> (loc * string) lazy tree | commitdiff
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
next
Unnamed repository; edit this file 'description' to name the repository.