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