projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2006-11-27
Andrea Asperti
Matita's default equality has changed
commit
|
commitdiff
|
tree
|
snapshot
2006-11-27
Andrea Asperti
Small changes
commit
|
commitdiff
|
tree
|
snapshot
2006-11-27
Claudio Sacerdoti...
auto new => auto new library in those tests that use...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-25
Enrico Tassi
fix
commit
|
commitdiff
|
tree
|
snapshot
2006-11-25
Enrico Tassi
patch to calculate meets of a pair of carriers
commit
|
commitdiff
|
tree
|
snapshot
2006-11-25
Enrico Tassi
added assertion (that is a TODO) in case non-considered...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-25
Enrico Tassi
added a test for the pullback stuff and the possibility...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Command index added to disambiguate.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Added a new command "index" for the indexing terms...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Set of Set of uri added.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Modifications to auto due to the introduction of the...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Universe is a discrimination-tree structure.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
The status has been extended with a "universe", that...
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Fixed a call to auto, and commented the remaining part.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
paramodulation removed
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Minor changes.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Simplified version.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-23
Andrea Asperti
Adding CoRN.
commit
|
commitdiff
|
tree
|
snapshot
2006-11-22
Ferruccio Guidi
removed the impredicativity of falsum
commit
|
commitdiff
|
tree
|
snapshot
2006-11-17
Claudio Sacerdoti...
Fixed the infamous bug:
commit
|
commitdiff
|
tree
|
snapshot
2006-11-17
Ferruccio Guidi
helm_registry: added the pair unmarshaller
commit
|
commitdiff
|
tree
|
snapshot
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
next