projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2006-10-31
Claudio Sacerdoti...
New behaviour of the disambiguation error messages...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-30
Claudio Sacerdoti...
TermAcicContent.Interpretation_not_found catched and...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-30
Claudio Sacerdoti...
Up to integration f-algebras.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-30
Claudio Sacerdoti...
Debugging code is now controlled by the debug flag.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-30
Andrea Asperti
library = yes!
commit
|
commitdiff
|
tree
|
snapshot
2006-10-30
Claudio Sacerdoti...
remove_obj is now much faster:
commit
|
commitdiff
|
tree
|
snapshot
2006-10-29
Ferruccio Guidi
Level-1/LambdaDelta now compiles fine
commit
|
commitdiff
|
tree
|
snapshot
2006-10-29
Claudio Sacerdoti...
Added target preall.opt.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-28
Claudio Sacerdoti...
GRAVE BUG IN COERCIONS FIXED: the insertion of a coerci...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-26
Claudio Sacerdoti...
Better label for the disambiguation errors window.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-26
Claudio Sacerdoti...
New (and much more complex) disambiguation error interface.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-26
Claudio Sacerdoti...
More timeout added to autos here and there.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Claudio Sacerdoti...
1. is_meta_closed should be applied only to terms on...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Ferruccio Guidi
till some patches
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Ferruccio Guidi
the incomplete proofs were axiomatized
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Ferruccio Guidi
some patches. still does not compile properly
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Claudio Sacerdoti...
Added timeouts to auto here and there.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Claudio Sacerdoti...
Added timeout to autos here and there.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Claudio Sacerdoti...
1. bug fixed: Unicode characters that are not mapped...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Claudio Sacerdoti...
/home/fguidi/... => ../../...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Ferruccio Guidi
we removed about 100 match-with costruction turning...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Andrea Asperti
Added a couple of flags to auto
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Claudio Sacerdoti...
Our unification used to guess a very complex argument...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-25
Claudio Sacerdoti...
Two lemmas that used to pass no more now pass again...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-24
Enrico Zoli
Added unit to rings.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-24
Enrico Zoli
More coercions added in the algebraic hierarchy.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-24
Enrico Zoli
Up to f_algebras.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-24
Enrico Tassi
fixed the ugly button added by csc, now it is inside...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-24
Enrico Tassi
removed equality_retrieval
commit
|
commitdiff
|
tree
|
snapshot
2006-10-23
Claudio Sacerdoti...
Better (and more localized) error message for sort_of_prod.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-23
Claudio Sacerdoti...
CicUniv.UniverseInconsistency is no handled correcly.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-23
Claudio Sacerdoti...
binaries/saturate no longer compiled since it does...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
Demodulate and applyS moved form saturation to auto.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
Major changes to auto, documented on the helm mailing...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
Minor changes.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
a. uniform mangement for context and library
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
The type of universe_of_goals has slightly changed...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
This is only a temporary patch. The typecheker raises a
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
The function exists_a_meta has been modified to capture...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Andrea Asperti
New function pack_coercion_metasenv, used in auto after...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Enrico Zoli
Up to f_algebras.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Enrico Zoli
1. developed up to algebras
commit
|
commitdiff
|
tree
|
snapshot
2006-10-20
Enrico Zoli
Serious bug fixed: without a Lazy.force the user obtain...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-19
Claudio Sacerdoti...
Disambiguation errors are now compressed in a maybe...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-19
Claudio Sacerdoti...
Bug fixed: when trying to insert coercions after an...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-19
Claudio Sacerdoti...
Potential performance improvement + better disambiguati...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
Missing optimization implemented: before starting to...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
- Disambiguation error exception enriched with more...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
Bug fixed: the diff component of the exception raised...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
EXPERIMENTAL: new interface for disambiguation errors.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
Dead dialog window removed.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
Dead dialog window removed.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
Disambiguation errors now carry more information (i...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
Dama is now in the night benchmarks.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-18
Claudio Sacerdoti...
Too verbose error message (probably activated by Enrico...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-17
Ferruccio Guidi
new objects for the LambdaDelta development (4th conjec...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-17
Ferruccio Guidi
more new objects for the LambdaDelta contribution
commit
|
commitdiff
|
tree
|
snapshot
2006-10-16
Enrico Zoli
Beginning of the development of integration algebras.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-13
Claudio Sacerdoti...
Content level representation of LetRec changed.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-13
Claudio Sacerdoti...
Content level representation of LetRec changed.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-13
Claudio Sacerdoti...
New content level representations for LetRec, Inductive...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Ferruccio Guidi
files with newest objects (to be included in the respec...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Enrico Tassi
carr_of_term now returns Fun if a Prod is encountered
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Enrico Tassi
fixed defaultauto behaviour. not the cache is preserveed
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Enrico Tassi
timeout if unspecfied should be set to infinity, not...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Claudio Sacerdoti...
The default for paramodulation is now back to false...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
acciavat
auto => auto new.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Claudio Sacerdoti...
Inclusion "improved".
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Claudio Sacerdoti...
CoRN integrated in the night benchmarks.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
acciavat
Manual porting of CoRN to Matita.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-12
Claudio Sacerdoti...
Bug fixed: the conversion was done with the wront argum...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-11
Claudio Sacerdoti...
Some hocus-pocus to avoid a common race condition ...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-11
Claudio Sacerdoti...
Unlocking the interface was not performed as the last...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-11
Claudio Sacerdoti...
The RELATIONAL contrib must be compiled before the...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-11
Claudio Sacerdoti...
My previous commit changed the regular timeout of param...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-10
Ferruccio Guidi
makefiles fixups
commit
|
commitdiff
|
tree
|
snapshot
2006-10-10
Claudio Sacerdoti...
fguidi removed from RT in makefiles
commit
|
commitdiff
|
tree
|
snapshot
2006-10-10
Claudio Sacerdoti...
Implemented:
commit
|
commitdiff
|
tree
|
snapshot
2006-10-10
Claudio Sacerdoti...
auto => auto new
commit
|
commitdiff
|
tree
|
snapshot
2006-10-10
Claudio Sacerdoti...
auto => auto new
commit
|
commitdiff
|
tree
|
snapshot
2006-10-10
Claudio Sacerdoti...
I do not understand at all why Enrico removed the contr...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-10
Claudio Sacerdoti...
Sorry, bug introduced by me yesterday now fixed.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
Bugs fixed in merging of composite coercions. In partic...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
One auto modified in an apply since auto is no longer...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
added to applyS in nat/gcd.ma a timeout large enough...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
1. applyS now uses its ~params
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
applyS now receives the same parameters that auto receives.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Andrea Asperti
Theorems from the library and from the context are...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
auto => auto new and other minor changes to make it...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
auto => auto new everywhere + minor updates to make...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
Comments updated with new reflections.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Andrea Asperti
The two coercions sym_eq e eq_f gives BIG TROUBLES...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Claudio Sacerdoti...
More work to handle -debug properly.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-09
Andrea Asperti
Factorized "find_equalities" in demodulation_tac.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-06
Enrico Tassi
added support for short name targets
commit
|
commitdiff
|
tree
|
snapshot
2006-10-06
Enrico Tassi
resumed ol auto
commit
|
commitdiff
|
tree
|
snapshot
2006-10-06
Enrico Tassi
fixed all (that now uses long paths)
commit
|
commitdiff
|
tree
|
snapshot
2006-10-06
Enrico Tassi
now the makefile for developments requires the depend...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-06
Claudio Sacerdoti...
1. some "try ... with _ " removed
commit
|
commitdiff
|
tree
|
snapshot
2006-10-03
Enrico Tassi
reduced timeout to 100s
commit
|
commitdiff
|
tree
|
snapshot
next