]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/ng_kernel
hints polished and fixed to allow recursive inference of ext_carr
[helm.git] / helm / software / components / ng_kernel /
2010-09-08 Enrico Tassibetter not allowed sort elimination error messsage
2010-05-12 Wilmer RicciottiExperimental support for Russell (coercions moving...
2010-05-06 Claudio Sacerdoti... assert false could happen
2010-03-24 Claudio Sacerdoti... ...
2010-02-09 Andrea AspertiAdded a count_occurrences function.
2010-02-04 Andrea AspertiAdded count_occurrences.
2010-02-03 Claudio Sacerdoti... Bug fixed: projection redexes obtained reducing other...
2010-01-27 Andrea AspertiAdded a parameter no_implicit (default true) to choose...
2009-12-09 Andrea AspertiAdded a "sort_metasenv" function.
2009-11-16 Wilmer RicciottiImplementation of ndestruct tactic (including destructi...
2009-11-13 Andrea AspertiExported apply_subst_context
2009-10-30 Claudio Sacerdoti... Sometimes it is useful to be able to print the subst...
2009-10-29 Claudio Sacerdoti... New function.
2009-10-22 Enrico Tassinew instantiate, only known bug is w.r.t. in/out scope...
2009-10-21 Enrico Tassipreserve sharing if map_term_fold_a
2009-10-20 Claudio Sacerdoti... - Bug fixed: some assert failure were just failures...
2009-10-16 Enrico Tassiremoved optimization potentially unsound
2009-10-14 Claudio Sacerdoti... Error message fixed (dereferencing must be done eagerly...
2009-10-14 Claudio Sacerdoti... Serious bug fixed: fix_sorts used to allow inference...
2009-10-13 Enrico Tassibetter ppcontext
2009-10-13 Enrico Tassibetter ppcontext
2009-10-08 Claudio Sacerdoti... A new switch to activate/deactive nCicReduction pretty...
2009-10-08 Claudio Sacerdoti... Printing extremely large terms no longer raises Failure.
2009-10-07 Claudio Sacerdoti... Performance improvement by preserving more sharing...
2009-10-07 Claudio Sacerdoti... - oCic2NCic and nCic2OCic moved to ng_library
2009-10-06 Wilmer RicciottiInverters/Inversion:
2009-10-05 Claudio Sacerdoti... ...
2009-10-05 Enrico Tassiadded auto_cache in the dupable status after an
2009-10-05 Enrico Tassinew ng_library module
2009-10-02 Enrico Tassifixed bug in coercion application, input/output swapped...
2009-10-02 Enrico Tassiprojections redex (proj (mk_foo ...)) where mk_foo
2009-10-02 Wilmer RicciottiUpdated command ninverter. Syntax:
2009-10-02 Claudio Sacerdoti... ...
2009-10-01 Enrico Tassifixed off-by-one
2009-09-30 Claudio Sacerdoti... New datatype for metasenv/subst: full fledged attribute...
2009-09-30 Wilmer RicciottiAdded initial support for inversion principles in Matit...
2009-09-28 Enrico Tassi- fixed bug in coercion application, input/output swapp...
2009-09-27 Enrico Tassifixpoint have attributes for pragma (i.e. they can...
2009-09-21 Enrico Tassihuge commit regarding universes:
2009-09-14 Enrico Tassifixed coercion mechanism w.r.t. undo/require
2009-09-14 Claudio Sacerdoti... Simplest typing for status records.
2009-09-09 Enrico Tassidepends
2009-09-09 Enrico Tassisome more work for ng-coercions
2009-09-04 Enrico TassiReduction speedup (a.k.a. better sharing):
2009-09-04 Enrico TassiReduction speedup (a.k.a. better sharing):
2009-09-01 Enrico Tassibetter print of ILLEGAL applications
2009-08-25 Enrico TassiMeta case not handled, the iterator was complaining.
2009-08-06 Claudio Sacerdoti... Metas must be handled when using iterators.
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.
next