]> matita.cs.unibo.it Git - helm.git/history - helm
New behaviour of fo_unif: in case of ?f args == t args'
[helm.git] / helm /
2010-01-24 Cosimo Oliboni freescale porting
2010-01-23 Cosimo Oliboni(no commit message)
2010-01-23 Cosimo Oliboni(no commit message)
2010-01-22 Cosimo Oliboni freescale porting
2010-01-22 Cosimo Oliboni freescale porting
2010-01-21 Cosimo Oliboni(no commit message)
2010-01-21 Andrea AspertiEsempio
2010-01-21 Cosimo Oliboni(no commit message)
2010-01-21 Cosimo Oliboni freescale porting, work in progress
2010-01-19 Claudio Sacerdoti... We can always use the "covered by emptyset" relation...
2010-01-18 Claudio Sacerdoti... More //.
2010-01-18 Claudio Sacerdoti... More // everywhere.
2010-01-18 Claudio Sacerdoti... // used everywhere!
2010-01-18 Claudio Sacerdoti... // in place of nauto everywhere
2010-01-18 Claudio Sacerdoti... // is now more powerful
2010-01-18 Claudio Sacerdoti... // is now more powerful
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-18 Andrea AspertiUpdating.
2010-01-15 Claudio Sacerdoti... A slightly more complicated example.
2010-01-15 Claudio Sacerdoti... Finished!
2010-01-15 Claudio Sacerdoti... We are still equivalent (even if the definition of...
2010-01-15 Claudio Sacerdoti... Urrah!
2010-01-15 Claudio Sacerdoti... Extending to the nAx set.
2010-01-15 Claudio Sacerdoti... Skipfact function (a partial general recursive function...
2010-01-12 Wilmer RicciottiFixed a bug in the discrimination principle: the refine...
2010-01-11 Claudio Sacerdoti... Finished
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 Claudio Sacerdoti... Improved
2010-01-08 Claudio Sacerdoti... Partial porting to new syntax.
2010-01-08 Claudio Sacerdoti... Source language path must be appended, not replaced.
2010-01-08 Claudio Sacerdoti... Categorical stuff postponed.
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 Aspertirebuilding the library
2010-01-08 Andrea Aspertirebuilding the library
2010-01-08 Andrea Aspertirebuilding the library
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.
2010-01-08 Andrea Aspertinew reloc_subst (to avoid cyclic substitutions).
2010-01-07 Enrico Tassi....
2010-01-07 Enrico Tassi...
2010-01-07 Enrico Tassi...
2010-01-06 Claudio Sacerdoti... Simplified.
2010-01-06 Claudio Sacerdoti... Coercions via unification hints?
2010-01-05 Ferruccio Guidi- we now add the kernel options in the preamble of...
2010-01-02 Claudio Sacerdoti... 1) stuff moved from categories.ma to setoids*.ma
2009-12-30 Enrico Tassi...
2009-12-30 Claudio Sacerdoti... Almost done (up to definition of category).
2009-12-30 Claudio Sacerdoti... Porting of Sambin's stuff started.
2009-12-30 Claudio Sacerdoti... Porting of Sambin's stuff started.
2009-12-30 Claudio Sacerdoti... Removed line is back again.
2009-12-30 Claudio Sacerdoti... ...
2009-12-21 Andrea AspertiRefining with no expected type + unification seems...
2009-12-21 Andrea AspertiTrying to be faster
2009-12-21 Andrea AspertiTrying to be faster.
2009-12-18 Andrea AspertiFinal subst returned by superposition and passed around.
2009-12-18 Andrea Aspertiusing = instead of alpha conversions. context metasenv...
2009-12-15 Andrea Aspertieq_coerc for smart application.
2009-12-14 Ferruccio Guidithe sort hierarchy parameter enter the kernel status
2009-12-10 Andrea AspertiMinor bag fixed, relative to failures.
2009-12-10 Andrea AspertiA compiling version?
2009-12-09 Andrea AspertiAdded a "sort_metasenv" function.
2009-12-09 Andrea AspertiCommented a couple of calls to "set_reference_of_oxuri".
2009-12-09 Andrea AspertiAdded the paramodulation stuff to the status
2009-12-09 Andrea Aspertiparam "slir" to call the new auto
2009-12-09 Andrea AspertiAdded the paramodulation active/passive tables to the...
2009-12-09 Andrea AspertiAttached fast_eq_check to auto
2009-12-09 Andrea AspertiAdded nnAuto.mli
2009-12-09 Andrea AspertiDebug set to ()
2009-12-09 Andrea AspertiClean up of debgging info
2009-12-09 Andrea AspertiSyntax error
2009-12-09 Andrea AspertiWrong reference corrected
2009-12-09 Andrea AspertiMinor fixing for last chance
2009-12-09 Andrea AspertiAdded a fol operation
2009-12-04 Wilmer RicciottiBugfix in inversion (was using refl_eq instead of refl).
2009-12-04 Andrea AspertiIndexing local context for paramod.
2009-12-02 Andrea AspertiPropositional equality
2009-12-02 Andrea AspertiThe new paramodulation functions instantiated over...
2009-12-02 Andrea AspertiNew ways for initialising the signature required for...
2009-12-02 Andrea AspertiPassive equations have their own index (not passive...
2009-12-02 Andrea Aspertidebug takes lazy strings. Moved here the are_alpha_eq...
2009-12-02 Andrea AspertiAdded a function remove_unit_clause
2009-12-02 Andrea AspertiAdded a boolean test function to discriminate equations...
2009-12-02 Andrea AspertiGeneralized intitialization for EqP
2009-12-02 Andrea AspertiGeneralized initialization of eqP.
2009-12-01 Enrico Tassiporting to lablgtk2 >= 2.14 and releasing
2009-12-01 Enrico Tassi...
2009-11-27 Wilmer Ricciottindestruct now clears off identity equations whenever...
2009-11-25 Wilmer RicciottiFixed inversion, which was broken by the last changes...
next