projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2006-11-17
Ferruccio Guidi
CoRN-Decl: missing file added
commit
|
commitdiff
|
tree
|
snapshot
2006-11-16
Ferruccio Guidi
- transcript: patched to generate CoRN_notation.ma...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-16
Ferruccio Guidi
- transcript: now outputs includes and coercions correctly
commit
|
commitdiff
|
tree
|
snapshot
2006-11-15
Ferruccio Guidi
new CoRN development, generated by transcript
commit
|
commitdiff
|
tree
|
snapshot
2006-11-15
Ferruccio Guidi
transcript updated
commit
|
commitdiff
|
tree
|
snapshot
2006-11-15
Ferruccio Guidi
removed prived CoRN configuration file :)
commit
|
commitdiff
|
tree
|
snapshot
2006-11-15
Ferruccio Guidi
transcript: very alpha version.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-15
Ferruccio Guidi
fixed base uri
commit
|
commitdiff
|
tree
|
snapshot
2006-11-15
Andrea Asperti
lt_O_S moved to nat/orders.ma
commit
|
commitdiff
|
tree
|
snapshot
2006-11-15
Andrea Asperti
Added lt_O_S.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-14
Claudio Sacerdoti...
&TODO => &TODO;
commit
|
commitdiff
|
tree
|
snapshot
2006-11-14
maiorino
New: on-line help for declarative tactics (first version).
commit
|
commitdiff
|
tree
|
snapshot
2006-11-14
Claudio Sacerdoti...
library=1 in obtain _ = _ by _.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-12
Claudio Sacerdoti...
The pretty printers in CicPp now have an optional ...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-11
Ferruccio Guidi
NLE is now derived fron NPlus rather than being a stand...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-10
Enrico Zoli
Dama: up to L-spaces and the proof (completed up to...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-06
Enrico Zoli
More work on groups, real numbers and integration algebras.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-05
Claudio Sacerdoti...
Some clean-up here and there in dama (coercions removed...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-05
Claudio Sacerdoti...
Almost every hand-inserted coercion removed since a...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-05
Claudio Sacerdoti...
Bug fixed: the disambiguation domain for a record with...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-05
Claudio Sacerdoti...
Critical bug finally found after a long chasing!!!
commit
|
commitdiff
|
tree
|
snapshot
2006-11-05
Claudio Sacerdoti...
Added more typing information to remove a coercion.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-03
Enrico Zoli
Integration f_algebras declassed.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-03
Enrico Zoli
Up to absolute value
commit
|
commitdiff
|
tree
|
snapshot
2006-11-03
Stefano Zacchiroli
preliminary support for hbugs
commit
|
commitdiff
|
tree
|
snapshot
2006-11-03
Enrico Zoli
Up to max (up to a bug).
commit
|
commitdiff
|
tree
|
snapshot
2006-10-31
Enrico Zoli
We begin to play the real game: we have defined real...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-31
Enrico Zoli
Integration_algebras.ma split into 6 different files.
commit
|
commitdiff
|
tree
|
snapshot
2006-10-31
Enrico Zoli
Syntax changed (to be changed back) for left parameters...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-31
Claudio Sacerdoti...
The OK button of the disambiguation errors interface...
commit
|
commitdiff
|
tree
|
snapshot
2006-10-31
Claudio Sacerdoti...
Bug fixed: inductive types were no longer removed from...
commit
|
commitdiff
|
tree
|
snapshot
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
next