]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
we started the implementation of higher order saturated sets
[helm.git] / helm / software / components /
2011-01-20 Wilmer RicciottiBug fix for generation of elimination principles.
2011-01-19 Wilmer RicciottiAdded some typing info to elimination principles, allow...
2010-12-10 Claudio Sacerdoti... Backporting from new Matita:
2010-12-03 Claudio Sacerdoti... Back-portin from new Matita: semantics of ntry changed...
2010-12-03 Claudio Sacerdoti... Back-porting from new Matita: improvement to inferred...
2010-12-02 Claudio Sacerdoti... Bad default for ?dorefine for instantiate
2010-12-02 Claudio Sacerdoti... 1. new implementation of normalize to have a speed...
2010-11-29 Claudio Sacerdoti... Bug fixed: propagation of left expected parameters...
2010-11-29 Claudio Sacerdoti... In the case type_of constructor with expected type...
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita:
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita:
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita:
2010-11-29 Claudio Sacerdoti... Back-porting from new matita:
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita:
2010-11-29 Claudio Sacerdoti... Back-porting from new Matita:
2010-11-23 Claudio Sacerdoti... Debugging code commented out.
2010-11-22 Claudio Sacerdoti... Debugging code commented out.
2010-11-22 Claudio Sacerdoti... Debugging code commented out.
2010-10-19 Enrico Tassicamlp5 probably changed some internal data structures...
2010-10-17 Enrico Tassifixed List.for_all2 called without knowing if the two...
2010-10-17 Enrico Tassinew case for higher order unification:
2010-10-17 Enrico Tassiremoved wrong optimization in delift and export is_flexible
2010-09-30 Enrico Tassipatches for hints & unification:
2010-09-12 Enrico TassiChange (or better define) the order of hints premises.
2010-09-08 Enrico Tassibetter not allowed sort elimination error messsage
2010-07-29 Claudio Sacerdoti... Bug fixed: nodes were copied.
2010-07-29 Enrico Tassiinterpret non ambiguous symbols ASAP
2010-07-28 Enrico Tassi...
2010-07-28 Enrico Tassiallows auto before eq is defined
2010-07-28 Wilmer RicciottiFixes unexpected behaviour of ncut when multiple goals...
2010-07-28 Wilmer RicciottiExperimental enhancements to the ndestruct tactic....
2010-07-22 Enrico Tassido not apply hints if metaclosed
2010-07-22 Enrico Tassiavoid assert false, just fail generating the coercion
2010-06-17 Enrico Tassioff by one fixed
2010-06-10 Wilmer RicciottiFix for inversion principles of types with a single...
2010-06-08 Wilmer RicciottiFixed a bug in the undebruijnate function which caused...
2010-06-07 Enrico Tassiunify left args of inductive types with left argus...
2010-05-12 Wilmer RicciottiExperimental support for Russell (coercions moving...
2010-05-10 Enrico Tassinew intro:
2010-05-07 Enrico Tassitrace generation with "// by _;"
2010-05-06 Claudio Sacerdoti... Bug fixed: nstatus => status (to undo the changes).
2010-05-06 Wilmer RicciottiFixing naming scheme for composite coercions.
2010-05-06 Claudio Sacerdoti... assert false could happen
2010-05-06 Claudio Sacerdoti... Bug fixed:
2010-05-04 Wilmer Ricciotti* Fixed a couple of glitches in ndestruct
2010-04-19 Andrea AspertiElimination of recursive inductive types leads to looping.
2010-04-19 Andrea Aspertialpha_eq instead of pervasives.compare
2010-04-13 Enrico Tassifixed makefile
2010-04-13 Enrico Tassiauto destructs while introducing in the context
2010-04-13 Enrico Tassiprint nobjects (hack with Obj.magic)
2010-04-13 Enrico Tassicatch the right exception, avoid uncaught Subst_not_found
2010-04-13 Enrico Tassisame heads different arity -> INCOMPARABLE
2010-04-13 Enrico Tassisome fixes to THF parser
2010-04-11 Ferruccio Guidithe edges must be quoted as well (not only the nodes)
2010-04-09 Andrea Aspertiapply_subst_context on statuses
2010-04-08 Enrico Tassisupport axioms
2010-04-08 Enrico Tassi...
2010-04-08 Enrico Tassithf problems list for tptp 4.0.1
2010-04-08 Enrico Tassifixed compiltion order of lexer/parser
2010-04-08 Claudio Sacerdoti... New code (unbranched) to compute all keys by all possib...
2010-04-08 Claudio Sacerdoti... New sets of.
2010-04-08 Enrico TassiTHF parser received some care
2010-04-08 Andrea AspertiFixing indexing (commit parziale di Claudio?)
2010-04-07 Enrico TassiTHF parser for TPTP
2010-03-31 Claudio Sacerdoti... Bug fixed: the current equation is not always the last...
2010-03-31 Claudio Sacerdoti... ...
2010-03-31 Claudio Sacerdoti... - inversion principles are now generated also for co...
2010-03-31 Claudio Sacerdoti... More debugging info from print_tac.
2010-03-31 Claudio Sacerdoti... Implicit and UserInput were printed incorrectly.
2010-03-31 Andrea AspertiTracing mechanism for auto. Interface changed to solve...
2010-03-25 Andrea AspertiExtension of demod to arbtrary predicates (not just...
2010-03-24 Claudio Sacerdoti... Equality has one right parameter and thus it's eliminat...
2010-03-24 Claudio Sacerdoti... ...
2010-03-24 Claudio Sacerdoti... Axioms were not indexed.
2010-03-24 Claudio Sacerdoti... Axioms were not indexed.
2010-03-24 Claudio Sacerdoti... ...
2010-03-24 Andrea AspertiComputation of the trace.
2010-03-23 Andrea AspertiFixed a few bugs
2010-03-23 Andrea Asperti"flat" function (subst unfolding)
2010-03-18 Andrea AspertiPrintings removed.
2010-03-18 Andrea AspertiDebugging disabled.
2010-03-18 Andrea AspertiDebugging disabled.
2010-03-18 Andrea AspertiNew demodulation tactics (mostly for debugging purposes).
2010-03-18 Andrea AspertiExporting the demodulation function.
2010-03-18 Andrea AspertiNew option "demod" for auto.
2010-03-18 Claudio Sacerdoti... Do not index examples (concrete syntax: nremark).
2010-03-18 Claudio Sacerdoti... nremark => `Example (not to be indexed)
2010-03-18 Andrea Aspertiapp of app inside smart application.
2010-03-17 Ferruccio Guididr
2010-03-17 Claudio Sacerdoti... OCaml's inferred type simplified.
2010-03-17 Claudio Sacerdoti... ...
2010-03-16 Claudio Sacerdoti... Comparison of two applications with a different number...
2010-03-16 Claudio Sacerdoti... 1) intros cleans up the cache (because the context...
2010-03-16 Claudio Sacerdoti... refreshing of inferred type was missing
2010-03-12 Andrea AspertiSubst was missing in perforate small (apparently, gty...
2010-03-12 Andrea Aspertiremoved debug from the inteface
2010-03-04 Andrea AspertiIn line with the ml.
2010-03-04 Andrea Asperti1. For smart application, we only perforate small terms...
2010-03-04 Andrea AspertiSmall changes for debugging
2010-03-04 Andrea AspertiFixed a bug in deep_eq: we generated new clauses but...
next