projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2010-03-18
Andrea Asperti
Porting the new definition of equality.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-18
Claudio Sacerdoti...
Do not index examples (concrete syntax: nremark).
commit
|
commitdiff
|
tree
|
snapshot
2010-03-18
Claudio Sacerdoti...
nremark => `Example (not to be indexed)
commit
|
commitdiff
|
tree
|
snapshot
2010-03-18
Andrea Asperti
app of app inside smart application.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-17
Ferruccio Guidi
dr
commit
|
commitdiff
|
tree
|
snapshot
2010-03-17
Andrea Asperti
qualche caso del lemma 5.2.11
commit
|
commitdiff
|
tree
|
snapshot
2010-03-17
Claudio Sacerdoti...
OCaml's inferred type simplified.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-17
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-17
Andrea Asperti
Splitted gpts in two files.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-17
Andrea Asperti
Aggiornamento alla negazione.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-17
Andrea Asperti
Nuova definizione della negazione.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-16
Claudio Sacerdoti...
Comparison of two applications with a different number...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-16
Claudio Sacerdoti...
1) intros cleans up the cache (because the context...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-16
Claudio Sacerdoti...
refreshing of inferred type was missing
commit
|
commitdiff
|
tree
|
snapshot
2010-03-16
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-12
Andrea Asperti
First version of PTS
commit
|
commitdiff
|
tree
|
snapshot
2010-03-12
Andrea Asperti
New definition of negation
commit
|
commitdiff
|
tree
|
snapshot
2010-03-12
Andrea Asperti
Subst was missing in perforate small (apparently, gty...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-12
Andrea Asperti
removed debug from the inteface
commit
|
commitdiff
|
tree
|
snapshot
2010-03-04
Andrea Asperti
In line with the ml.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-04
Andrea Asperti
1. For smart application, we only perforate small terms...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-04
Andrea Asperti
Small changes for debugging
commit
|
commitdiff
|
tree
|
snapshot
2010-03-04
Andrea Asperti
Fixed a bug in deep_eq: we generated new clauses but...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-04
Andrea Asperti
Corrected a bug relative to the application of substs...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-02
Wilmer Ricciotti
Added reverse rewriting principle in Type[0].
commit
|
commitdiff
|
tree
|
snapshot
2010-03-02
Wilmer Ricciotti
Some integrations to the ng library.
commit
|
commitdiff
|
tree
|
snapshot
2010-03-02
Wilmer Ricciotti
Added syntax for ninversion tactic (still experimental).
commit
|
commitdiff
|
tree
|
snapshot
2010-03-02
Enrico Tassi
Constants are indexed using the Reference, not the...
commit
|
commitdiff
|
tree
|
snapshot
2010-03-01
Wilmer Ricciotti
Fixed a bug in the unification, which prevented some...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-25
Ferruccio Guidi
-bugfix in the "profile" entry
commit
|
commitdiff
|
tree
|
snapshot
2010-02-25
Ferruccio Guidi
- pipeline support for generated entities in text mode...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-25
Wilmer Ricciotti
Minimal example in Z showing a problem in the nnormaliz...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-24
Ferruccio Guidi
- a couple of new entities
commit
|
commitdiff
|
tree
|
snapshot
2010-02-23
Ferruccio Guidi
- the text model now supports invocations of the entity...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-22
Ferruccio Guidi
- we completed the text parser fixing the syntactic...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-21
Ferruccio Guidi
- we added some syntactic sugar in the text parser
commit
|
commitdiff
|
tree
|
snapshot
2010-02-20
Ferruccio Guidi
- we implemented the hierarchy and sort names declarati...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
Open goals fixed (it also returned closed goals).
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Ferruccio Guidi
- we added a parser for lambda-delta textual syntax...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
Removed debug printings.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
added lazy
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
Nuova versione di auto.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
New proofs.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
Wilmer's stuff for destruct.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
(no commit message)
commit
|
commitdiff
|
tree
|
snapshot
2010-02-19
Andrea Asperti
Added an implicit parameter to branch_tac to allow...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-16
Andrea Asperti
More theorems
commit
|
commitdiff
|
tree
|
snapshot
2010-02-16
Andrea Asperti
Minor fixings.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-15
Claudio Sacerdoti...
The height of fixpoint applications was not computed...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-12
Cosimo Oliboni
cerco documentation
commit
|
commitdiff
|
tree
|
snapshot
2010-02-11
Enrico Tassi
minimal sequent height set to 1
commit
|
commitdiff
|
tree
|
snapshot
2010-02-11
Enrico Tassi
some experiment filtering with height
commit
|
commitdiff
|
tree
|
snapshot
2010-02-10
Andrea Asperti
addenda
commit
|
commitdiff
|
tree
|
snapshot
2010-02-09
Andrea Asperti
Added a count_occurrences function.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-08
Andrea Asperti
Bug fixing.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-08
Andrea Asperti
Removed debug printings.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-08
Andrea Asperti
Some changes towards integration of setoid-rewriting.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-06
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-02-06
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-02-05
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-02-04
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-04
Andrea Asperti
Added count_occurrences.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-04
Andrea Asperti
Bug fixed: goto_top used to reset the status to the...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-04
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-02-04
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
End of curryfication of binary_morphisms.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Curryfication of binary_morphisms.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Curryfication of binary setoids.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Curryfication of binary morphisms.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Work in Progress: Who needs binary_morphisms? Curryfica...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Wilmer Ricciotti
Disabled debug prints in ndestruct tactic.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Debug code commented out.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Parts of the status were not re-initialized correctly...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Bad variable name fixed.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-03
Claudio Sacerdoti...
Bug fixed: projection redexes obtained reducing other...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Wilmer Ricciotti
New version using Streicher's K axiom. Should be faster...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Wilmer Ricciotti
Added Streicher's K axiom.
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Wilmer Ricciotti
Fixed a bug with indexed inductive types which sometime...
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Andrea Asperti
lists
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Andrea Asperti
Booleans
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Andrea Asperti
boolean arithmetics
commit
|
commitdiff
|
tree
|
snapshot
2010-02-02
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-02-01
Cosimo Oliboni
(no commit message)
commit
|
commitdiff
|
tree
|
snapshot
2010-02-01
Andrea Asperti
minus
commit
|
commitdiff
|
tree
|
snapshot
2010-02-01
Andrea Asperti
On the last goal at maxdepth we stop at the first solution.
commit
|
commitdiff
|
tree
|
snapshot
2010-01-31
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-01-30
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-01-30
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-01-29
Andrea Asperti
minus in nat.ma
commit
|
commitdiff
|
tree
|
snapshot
2010-01-29
Andrea Asperti
Nuova gestione della width.
commit
|
commitdiff
|
tree
|
snapshot
2010-01-29
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-01-28
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-01-27
Andrea Asperti
le_arith
commit
|
commitdiff
|
tree
|
snapshot
2010-01-27
Andrea Asperti
Unfolded exact letins during proof reconstruction.
commit
|
commitdiff
|
tree
|
snapshot
2010-01-27
Andrea Asperti
Added a parameter no_implicit (default true) to choose...
commit
|
commitdiff
|
tree
|
snapshot
2010-01-27
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
2010-01-26
Andrea Asperti
le_arith
commit
|
commitdiff
|
tree
|
snapshot
2010-01-25
Cosimo Oliboni
freescale porting
commit
|
commitdiff
|
tree
|
snapshot
next