]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
fixed makefile
[helm.git] / helm / software / components /
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...
2010-03-04 Andrea AspertiCorrected a bug relative to the application of substs...
2010-03-02 Wilmer RicciottiAdded syntax for ninversion tactic (still experimental).
2010-03-02 Enrico TassiConstants are indexed using the Reference, not the...
2010-03-01 Wilmer RicciottiFixed a bug in the unification, which prevented some...
2010-02-19 Andrea AspertiOpen goals fixed (it also returned closed goals).
2010-02-19 Andrea AspertiRemoved debug printings.
2010-02-19 Andrea Aspertiadded lazy
2010-02-19 Andrea AspertiNuova versione di auto.
2010-02-19 Andrea AspertiAdded an implicit parameter to branch_tac to allow...
2010-02-15 Claudio Sacerdoti... The height of fixpoint applications was not computed...
2010-02-11 Enrico Tassiminimal sequent height set to 1
2010-02-11 Enrico Tassisome experiment filtering with height
2010-02-09 Andrea AspertiAdded a count_occurrences function.
2010-02-08 Andrea AspertiBug fixing.
2010-02-08 Andrea AspertiRemoved debug printings.
2010-02-08 Andrea AspertiSome changes towards integration of setoid-rewriting.
2010-02-04 Andrea AspertiAdded count_occurrences.
2010-02-03 Claudio Sacerdoti... ...
2010-02-03 Wilmer RicciottiDisabled debug prints in ndestruct tactic.
2010-02-03 Claudio Sacerdoti... Debug code commented out.
2010-02-03 Claudio Sacerdoti... Parts of the status were not re-initialized correctly...
2010-02-03 Claudio Sacerdoti... Bad variable name fixed.
2010-02-03 Claudio Sacerdoti... Bug fixed: projection redexes obtained reducing other...
2010-02-02 Wilmer RicciottiNew version using Streicher's K axiom. Should be faster...
2010-02-02 Wilmer RicciottiFixed a bug with indexed inductive types which sometime...
2010-02-01 Andrea AspertiOn the last goal at maxdepth we stop at the first solution.
2010-01-29 Andrea AspertiNuova gestione della width.
2010-01-27 Andrea AspertiUnfolded exact letins during proof reconstruction.
2010-01-27 Andrea AspertiAdded a parameter no_implicit (default true) to choose...
2010-01-18 Andrea AspertiNew paramod tac.
2010-01-18 Andrea AspertiInvocation of paramod
2010-01-18 Andrea Aspertiparamod_tac exported
2010-01-18 Andrea AspertiNumber notation for NG
2010-01-18 Andrea AspertiNumber notation for NG
2010-01-18 Andrea AspertiNumber notation for NG.
2010-01-18 Andrea AspertiKeeping Implicit for refinement (instead of transformin...
2010-01-12 Wilmer RicciottiFixed a bug in the discrimination principle: the refine...
2010-01-11 Andrea Asperti1. New paramodulation function
2010-01-11 Andrea Aspertisaturate cust be called with delta=0
2010-01-11 Andrea AspertiAdded is_equation
2010-01-11 Andrea AspertiDebugging info
2010-01-08 Andrea AspertiThe body of constants is a reference, not the actual...
2010-01-08 Andrea Aspertiremoved debugging info
2010-01-08 Andrea AspertiapplyS
2010-01-08 Andrea Aspertirefresh uri
2010-01-08 Andrea AspertiSupport for the new auto tactics //
2010-01-08 Andrea AspertiSupport for the new // tactics.
next