]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_kernel
\ldots are now used in nelim and ncases
[helm.git] / helm / software / components / ng_kernel /
2009-07-31 Claudio Sacerdoti... Pp fixed in order to obtain read-back.
2009-07-28 Claudio Sacerdoti... "..." -> "\ldots" for implicit vectors
2009-07-28 Claudio Sacerdoti... Introduction of vectors of implicit (only for NG).
2009-07-27 Claudio Sacerdoti... Serious bug fixed: because of lazy evaluation of !requi...
2009-07-20 Claudio Sacerdoti... 1) The NG kernel now accepts only usage of declared...
2009-07-17 Claudio Sacerdoti... 1) added a function to retrieve all the universes curre...
2009-07-08 Claudio Sacerdoti... Metavariable case in does_not_occur (hence weakly/stric...
2009-07-08 Claudio Sacerdoti... Missing case for Match implemented.
2009-07-08 Claudio Sacerdoti... weakly/strictly positive checks relaxed to allow metava...
2009-07-08 Claudio Sacerdoti... Bug fixed: the debrujinate function (hence the one...
2009-07-07 Claudio Sacerdoti... Bug fixed: one uri was not refreshed, causing divergenc...
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces...
2009-06-23 Enrico Tassiundo/serialization for universes implemented
2009-06-23 Claudio Sacerdoti... Debugging prerr_endlines removed.
2009-06-23 Claudio Sacerdoti... 1) NCicTypechecker.typecheck_obj removed, since it...
2009-06-23 Claudio Sacerdoti... - Bug fixed: removed URIs were not removed from the...
2009-06-21 Ferruccio Guidi- cicNotationPp: bugfix in record syntax
2009-06-20 Claudio Sacerdoti... Debugging
2009-06-19 Claudio Sacerdoti... Invert dependencies between baseuris (files) are now...
2009-06-19 Claudio Sacerdoti... Bug fixed: refreshing of uris for the db.
2009-06-19 Claudio Sacerdoti... The global db is now updated during decompilation.
2009-06-19 Claudio Sacerdoti... Persistent db (to lookup names in the library) ineffici...
2009-06-19 Claudio Sacerdoti... NG decompilation is now activated. However, it is calle...
2009-06-19 Claudio Sacerdoti... Good:
2009-06-18 Claudio Sacerdoti... Objects are now used to represent also the tactic status.
2009-06-17 Claudio Sacerdoti... Initial implementation of statuses using objects in...
2009-06-16 Claudio Sacerdoti... 1) unification hint now takes NG terms (as it should...
2009-06-16 Claudio Sacerdoti... 1) NCicLibrary (which is untrusted) moved after NCicUnt...
2009-06-16 Claudio Sacerdoti... Implementation of existential type improved (more stric...
2009-06-16 Claudio Sacerdoti... FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
2009-06-15 Enrico TassiEXPERIMENTAL COMMIT (part B, by CSC :-):
2009-06-15 Enrico TassiEXPERIMENTAL COMMIT (by CSC,actuall :-)
2009-06-15 Enrico Tassihuge commit regarding the grafite_status:
2009-06-05 denesFix : wrong exception was catch in apply_subst
2009-06-05 Claudio Sacerdoti... The kernel _must_ check the correctness of the height...
2009-06-03 Claudio Sacerdoti... Huge commit with several changes:
2009-05-25 Enrico Tassinasty change in the lexer/parser:
2009-05-18 Enrico Tassiremoved useless function
2009-05-18 Enrico Tassiin the new kernel you can type Type[i] to mean Type_i...
2009-05-18 Enrico Tassinothing special
2009-05-17 Claudio Sacerdoti... alpha_eq exported
2009-05-17 Claudio Sacerdoti... alpha_eq defined and exported
2009-05-17 Claudio Sacerdoti... efficiency improvement (buffers are now used everywhere)
2009-05-15 Claudio Sacerdoti... Patch to add a debugging string to HExtlib.split_nth...
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth
2009-05-11 Claudio Sacerdoti... ppsubst commented out in ppobj
2009-05-11 Claudio Sacerdoti... Buffers are now used everywhere for speed-up.
2009-05-10 Claudio Sacerdoti... - critical bug fixed in NCicSubstitution.lift:
2009-05-08 Claudio Sacerdoti... ...
2009-05-08 Claudio Sacerdoti... The relevance list can be shorter than leftno (when...
2009-05-05 Enrico Tassi- pretty printer made robust in face of list_nth
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!
next