]> 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
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 tree | commitdiff
2010-05-12 Wilmer RicciottiExperimental support for Russell (coercions moving... tree | commitdiff
2010-05-06 Claudio Sacerdoti... assert false could happen tree | commitdiff
2010-03-24 Claudio Sacerdoti... ... tree | commitdiff
2010-02-09 Andrea AspertiAdded a count_occurrences function. tree | commitdiff
2010-02-04 Andrea AspertiAdded count_occurrences. tree | commitdiff
2010-02-03 Claudio Sacerdoti... Bug fixed: projection redexes obtained reducing other... tree | commitdiff
2010-01-27 Andrea AspertiAdded a parameter no_implicit (default true) to choose... tree | commitdiff
2009-12-09 Andrea AspertiAdded a "sort_metasenv" function. tree | commitdiff
2009-11-16 Wilmer RicciottiImplementation of ndestruct tactic (including destructi... tree | commitdiff
2009-11-13 Andrea AspertiExported apply_subst_context tree | commitdiff
2009-10-30 Claudio Sacerdoti... Sometimes it is useful to be able to print the subst... tree | commitdiff
2009-10-29 Claudio Sacerdoti... New function. tree | commitdiff
2009-10-22 Enrico Tassinew instantiate, only known bug is w.r.t. in/out scope... tree | commitdiff
2009-10-21 Enrico Tassipreserve sharing if map_term_fold_a tree | commitdiff
2009-10-20 Claudio Sacerdoti... - Bug fixed: some assert failure were just failures... tree | commitdiff
2009-10-16 Enrico Tassiremoved optimization potentially unsound tree | commitdiff
2009-10-14 Claudio Sacerdoti... Error message fixed (dereferencing must be done eagerly... tree | commitdiff
2009-10-14 Claudio Sacerdoti... Serious bug fixed: fix_sorts used to allow inference... tree | commitdiff
2009-10-13 Enrico Tassibetter ppcontext tree | commitdiff
2009-10-13 Enrico Tassibetter ppcontext tree | commitdiff
2009-10-08 Claudio Sacerdoti... A new switch to activate/deactive nCicReduction pretty... tree | commitdiff
2009-10-08 Claudio Sacerdoti... Printing extremely large terms no longer raises Failure. tree | commitdiff
2009-10-07 Claudio Sacerdoti... Performance improvement by preserving more sharing... tree | commitdiff
2009-10-07 Claudio Sacerdoti... - oCic2NCic and nCic2OCic moved to ng_library tree | commitdiff
2009-10-06 Wilmer RicciottiInverters/Inversion: tree | commitdiff
2009-10-05 Claudio Sacerdoti... ... tree | commitdiff
2009-10-05 Enrico Tassiadded auto_cache in the dupable status after an tree | commitdiff
2009-10-05 Enrico Tassinew ng_library module tree | commitdiff
2009-10-02 Enrico Tassifixed bug in coercion application, input/output swapped... tree | commitdiff
2009-10-02 Enrico Tassiprojections redex (proj (mk_foo ...)) where mk_foo tree | commitdiff
2009-10-02 Wilmer RicciottiUpdated command ninverter. Syntax: tree | commitdiff
2009-10-02 Claudio Sacerdoti... ... tree | commitdiff
2009-10-01 Enrico Tassifixed off-by-one tree | commitdiff
2009-09-30 Claudio Sacerdoti... New datatype for metasenv/subst: full fledged attribute... tree | commitdiff
2009-09-30 Wilmer RicciottiAdded initial support for inversion principles in Matit... tree | commitdiff
2009-09-28 Enrico Tassi- fixed bug in coercion application, input/output swapp... tree | commitdiff
2009-09-27 Enrico Tassifixpoint have attributes for pragma (i.e. they can... tree | commitdiff
2009-09-21 Enrico Tassihuge commit regarding universes: tree | commitdiff
2009-09-14 Enrico Tassifixed coercion mechanism w.r.t. undo/require tree | commitdiff
2009-09-14 Claudio Sacerdoti... Simplest typing for status records. tree | commitdiff
2009-09-09 Enrico Tassidepends tree | commitdiff
2009-09-09 Enrico Tassisome more work for ng-coercions tree | commitdiff
2009-09-04 Enrico TassiReduction speedup (a.k.a. better sharing): tree | commitdiff
2009-09-04 Enrico TassiReduction speedup (a.k.a. better sharing): tree | commitdiff
2009-09-01 Enrico Tassibetter print of ILLEGAL applications tree | commitdiff
2009-08-25 Enrico TassiMeta case not handled, the iterator was complaining. tree | commitdiff
2009-08-06 Claudio Sacerdoti... Metas must be handled when using iterators. tree | commitdiff
2009-07-31 Claudio Sacerdoti... Pp fixed in order to obtain read-back. tree | commitdiff
2009-07-28 Claudio Sacerdoti... "..." -> "\ldots" for implicit vectors tree | commitdiff
2009-07-28 Claudio Sacerdoti... Introduction of vectors of implicit (only for NG). tree | commitdiff
2009-07-27 Claudio Sacerdoti... Serious bug fixed: because of lazy evaluation of !requi... tree | commitdiff
2009-07-20 Claudio Sacerdoti... 1) The NG kernel now accepts only usage of declared... tree | commitdiff
2009-07-17 Claudio Sacerdoti... 1) added a function to retrieve all the universes curre... tree | commitdiff
2009-07-08 Claudio Sacerdoti... Metavariable case in does_not_occur (hence weakly/stric... tree | commitdiff
2009-07-08 Claudio Sacerdoti... Missing case for Match implemented. tree | commitdiff
2009-07-08 Claudio Sacerdoti... weakly/strictly positive checks relaxed to allow metava... tree | commitdiff
2009-07-08 Claudio Sacerdoti... Bug fixed: the debrujinate function (hence the one... tree | commitdiff
2009-07-07 Claudio Sacerdoti... Bug fixed: one uri was not refreshed, causing divergenc... tree | commitdiff
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces... tree | commitdiff
2009-06-23 Enrico Tassiundo/serialization for universes implemented tree | commitdiff
2009-06-23 Claudio Sacerdoti... Debugging prerr_endlines removed. tree | commitdiff
2009-06-23 Claudio Sacerdoti... 1) NCicTypechecker.typecheck_obj removed, since it... tree | commitdiff
2009-06-23 Claudio Sacerdoti... - Bug fixed: removed URIs were not removed from the... tree | commitdiff
2009-06-21 Ferruccio Guidi- cicNotationPp: bugfix in record syntax tree | commitdiff
2009-06-20 Claudio Sacerdoti... Debugging tree | commitdiff
2009-06-19 Claudio Sacerdoti... Invert dependencies between baseuris (files) are now... tree | commitdiff
2009-06-19 Claudio Sacerdoti... Bug fixed: refreshing of uris for the db. tree | commitdiff
2009-06-19 Claudio Sacerdoti... The global db is now updated during decompilation. tree | commitdiff
2009-06-19 Claudio Sacerdoti... Persistent db (to lookup names in the library) ineffici... tree | commitdiff
2009-06-19 Claudio Sacerdoti... NG decompilation is now activated. However, it is calle... tree | commitdiff
2009-06-19 Claudio Sacerdoti... Good: tree | commitdiff
2009-06-18 Claudio Sacerdoti... Objects are now used to represent also the tactic status. tree | commitdiff
2009-06-17 Claudio Sacerdoti... Initial implementation of statuses using objects in... tree | commitdiff
2009-06-16 Claudio Sacerdoti... 1) unification hint now takes NG terms (as it should... tree | commitdiff
2009-06-16 Claudio Sacerdoti... 1) NCicLibrary (which is untrusted) moved after NCicUnt... tree | commitdiff
2009-06-16 Claudio Sacerdoti... Implementation of existential type improved (more stric... tree | commitdiff
2009-06-16 Claudio Sacerdoti... FIX OF THE PREVIOUS EXPERIMENTAL COMMIT: tree | commitdiff
2009-06-15 Enrico TassiEXPERIMENTAL COMMIT (part B, by CSC :-): tree | commitdiff
2009-06-15 Enrico TassiEXPERIMENTAL COMMIT (by CSC,actuall :-) tree | commitdiff
2009-06-15 Enrico Tassihuge commit regarding the grafite_status: tree | commitdiff
2009-06-05 denesFix : wrong exception was catch in apply_subst tree | commitdiff
2009-06-05 Claudio Sacerdoti... The kernel _must_ check the correctness of the height... tree | commitdiff
2009-06-03 Claudio Sacerdoti... Huge commit with several changes: tree | commitdiff
2009-05-25 Enrico Tassinasty change in the lexer/parser: tree | commitdiff
2009-05-18 Enrico Tassiremoved useless function tree | commitdiff
2009-05-18 Enrico Tassiin the new kernel you can type Type[i] to mean Type_i... tree | commitdiff
2009-05-18 Enrico Tassinothing special tree | commitdiff
2009-05-17 Claudio Sacerdoti... alpha_eq exported tree | commitdiff
2009-05-17 Claudio Sacerdoti... alpha_eq defined and exported tree | commitdiff
2009-05-17 Claudio Sacerdoti... efficiency improvement (buffers are now used everywhere) tree | commitdiff
2009-05-15 Claudio Sacerdoti... Patch to add a debugging string to HExtlib.split_nth... tree | commitdiff
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth tree | commitdiff
2009-05-11 Claudio Sacerdoti... ppsubst commented out in ppobj tree | commitdiff
2009-05-11 Claudio Sacerdoti... Buffers are now used everywhere for speed-up. tree | commitdiff
2009-05-10 Claudio Sacerdoti... - critical bug fixed in NCicSubstitution.lift: tree | commitdiff
2009-05-08 Claudio Sacerdoti... ... tree | commitdiff
2009-05-08 Claudio Sacerdoti... The relevance list can be shorter than leftno (when... tree | commitdiff
2009-05-05 Enrico Tassi- pretty printer made robust in face of list_nth tree | commitdiff
2009-04-29 Claudio Sacerdoti... Refinement of inductive type implemented. tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.