]> matita.cs.unibo.it Git - helm.git/history - helm/software/components
projects / helm.git / history
? search:
summary | shortlog | log | commit | commitdiff | tree
first ⋅ prev ⋅ next
- oCic2NCic and nCic2OCic moved to ng_library
[helm.git] / helm / software / components /
2009-07-24 Claudio Sacerdoti... Record fields declared as coercions as now really decla... tree | commitdiff
2009-07-24 Claudio Sacerdoti... Beta-expansion was avoided as soon as one argument... tree | commitdiff
2009-07-24 Claudio Sacerdoti... Function to map NCic.term to CicNotationPt.term finished. tree | commitdiff
2009-07-24 Claudio Sacerdoti... Bug (found during code review) fixed (but not tested... tree | commitdiff
2009-07-22 Claudio Sacerdoti... Major speed-up: meta-chains are now expanded during... tree | commitdiff
2009-07-22 denesFixed test for invertibility tree | commitdiff
2009-07-22 denesNow using lazy strings for debug printings tree | commitdiff
2009-07-22 Claudio Sacerdoti... leftno was List.length rights :-) tree | commitdiff
2009-07-22 Claudio Sacerdoti... Almost ready to implement coercion declaration for... tree | commitdiff
2009-07-21 Claudio Sacerdoti... Debugging code removed. tree | commitdiff
2009-07-21 Claudio Sacerdoti... Record projections are now automatically generated... tree | commitdiff
2009-07-21 denesImplemented handling of Invertible equalities tree | commitdiff
2009-07-20 Enrico Tassisorted modules tree | commitdiff
2009-07-20 Claudio Sacerdoti... Debugging printf removed tree | commitdiff
2009-07-20 Claudio Sacerdoti... nrewrite now uses the appropriate principle when going... tree | commitdiff
2009-07-20 denesRemoved status printing by processes tree | commitdiff
2009-07-20 denesFixed multiple printing tree | commitdiff
2009-07-20 Wilmer RicciottiFinal version, submitted to CASC-22. tree | commitdiff
2009-07-20 Wilmer Ricciottiadded a flag for age selection tree | commitdiff
2009-07-20 Claudio Sacerdoti... Very serious bug fixed in unification, but the fix... tree | commitdiff
2009-07-20 Claudio Sacerdoti... 1) The NG kernel now accepts only usage of declared... tree | commitdiff
2009-07-20 denesOne-side indexing for commutativity tree | commitdiff
2009-07-20 denesNo demod call on functionnal symbols tree | commitdiff
2009-07-20 Claudio Sacerdoti... 1) ppmetasenv and ppcontext to reduce the amount of... tree | commitdiff
2009-07-17 Claudio Sacerdoti... nelim now uses the appropriate _rect_XXX elimination... tree | commitdiff
2009-07-17 Claudio Sacerdoti... 1) the user is notified when a new object is defined tree | commitdiff
2009-07-17 Claudio Sacerdoti... More info to refine empty types elimination. tree | commitdiff
2009-07-17 Claudio Sacerdoti... Generation of principles is now atomic. tree | commitdiff
2009-07-17 Claudio Sacerdoti... Debugging code commented out. tree | commitdiff
2009-07-17 Enrico Tassiadd comment tree | commitdiff
2009-07-17 Claudio Sacerdoti... Bug fixed: singleton application. tree | commitdiff
2009-07-17 Claudio Sacerdoti... New suffixes for elimination principles: tree | commitdiff
2009-07-17 Claudio Sacerdoti... 1) added a function to retrieve all the universes curre... tree | commitdiff
2009-07-17 Claudio Sacerdoti... Generation of inductive principle for Type[0]. tree | commitdiff
2009-07-16 denesSorted version of eligible problems list tree | commitdiff
2009-07-16 denesDisabled age selection and ad hoc goal weight computation tree | commitdiff
2009-07-15 Enrico Tassincopy partially implemented and fixed (a ?) chain to... tree | commitdiff
2009-07-15 Wilmer RicciottiFixed dependency function, which was lacking the code... tree | commitdiff
2009-07-15 Enrico Tassi... tree | commitdiff
2009-07-15 Enrico Tassimatch_coercion gives back the saturations, not the... tree | commitdiff
2009-07-14 denesFixed Option type error (OCaml bug) tree | commitdiff
2009-07-14 denes. tree | commitdiff
2009-07-14 denes. tree | commitdiff
2009-07-13 Enrico Tassibetter spacing tree | commitdiff
2009-07-13 Enrico Tassistatistics are used, when possible, to sort tree | commitdiff
2009-07-13 denesAdded statistics printings tree | commitdiff
2009-07-13 denesAdded statistics module tree | commitdiff
2009-07-13 Enrico Tassimatitaprover is now flexible enough to allow the comput... tree | commitdiff
2009-07-13 Claudio Sacerdoti... Coercion hiding implemented. Notes: tree | commitdiff
2009-07-10 Enrico Tassiinitial implementation of coercion composition tree | commitdiff
2009-07-10 denesRemoved unused parameter of unification procedure ... tree | commitdiff
2009-07-10 Enrico Tassimore profilers tree | commitdiff
2009-07-10 Claudio Sacerdoti... Bug fixed (missing ctx) + comment added. tree | commitdiff
2009-07-09 Enrico Tassiinitial implementation of `ncoercion name : type :... tree | commitdiff
2009-07-09 Enrico Tassinew nrepeat (and block '('...')' ) tactical tree | commitdiff
2009-07-09 Enrico TassiNew functorialization: paramod is abstracted over a... tree | commitdiff
2009-07-09 denesFixed check for condition iv p.33 (Riazzanov) tree | commitdiff
2009-07-09 Enrico Tassiprofile most operations, do not return a filtered varli... tree | commitdiff
2009-07-09 Enrico Tassi1 process for now tree | commitdiff
2009-07-09 Enrico Tassitwo cases should be assert false at least in TPTP tree | commitdiff
2009-07-09 Enrico Tassimicro optimizations to unification tree | commitdiff
2009-07-09 denesCleaned a bit tree | commitdiff
2009-07-09 Enrico Tassi... tree | commitdiff
2009-07-09 Enrico Tassiactivate kbo, not lpo tree | commitdiff
2009-07-09 Claudio Sacerdoti... Bug fixed (non-captured variable). tree | commitdiff
2009-07-08 Claudio Sacerdoti... repeat_tac 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... Improved error message. 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-07-06 denesFixed printing of number of problems solved tree | commitdiff
2009-07-06 denesTried to implement lpo in a more efficient way tree | commitdiff
2009-07-06 denesFixed typo in lpo (from old implementation) tree | commitdiff
2009-07-03 denesPorted old implementation of LPO (for test purposes) tree | commitdiff
2009-07-03 denesImplemented LPO tree | commitdiff
2009-07-02 denesCorrected type for bag tree | commitdiff
2009-07-02 denesNew age selection tree | commitdiff
2009-07-02 Enrico Tassibetter output handling tree | commitdiff
2009-07-02 Enrico Tassireturn type of paramod fixed according to the SZSOntology tree | commitdiff
2009-07-01 Enrico Tassi... tree | commitdiff
2009-07-01 Enrico Tassi... tree | commitdiff
2009-07-01 Wilmer RicciottiVersion number set to 1.0.0-rc1 tree | commitdiff
2009-07-01 denesFixed type of bag tree | commitdiff
2009-06-30 Enrico Tassiparallel tree | commitdiff
2009-06-30 denesMoved ID management inside the bag tree | commitdiff
2009-06-30 Enrico Tassiattempt of using 2 different orderings tree | commitdiff
2009-06-30 Enrico Tassi.... tree | commitdiff
2009-06-30 denesCorrected a few typos tree | commitdiff
2009-06-30 Enrico Tassi... tree | commitdiff
2009-06-30 denesEnabled age selection (ratio 1/5) tree | commitdiff
2009-06-29 Enrico Tassi... tree | commitdiff
2009-06-29 Enrico Tassido not infer on closed goals tree | commitdiff
2009-06-29 Enrico Tassi... tree | commitdiff
2009-06-29 denesFirst attempt for refined goal selection strategy tree | commitdiff
2009-06-29 Enrico Tassiadded (but not active) last chance idea tree | commitdiff
2009-06-29 denesImplemented orphan murdering technique tree | commitdiff
2009-06-29 Enrico Tassinew make test target tree | commitdiff
next
Unnamed repository; edit this file 'description' to name the repository.