projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2014-05-25
Ferruccio Guidi
update in ground_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-25
Ferruccio Guidi
- theory of llor now includes (long awaited) non-recurs...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-24
Ferruccio Guidi
non-recursive alternative of llpx_sn completed !
commit
|
commitdiff
|
tree
|
snapshot
2014-05-23
Ferruccio Guidi
update in grond_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-23
Ferruccio Guidi
advances on cofrees allows to prove one direction of
commit
|
commitdiff
|
tree
|
snapshot
2014-05-11
Ferruccio Guidi
update in ground_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-05-11
Ferruccio Guidi
advances on ldrop ....
commit
|
commitdiff
|
tree
|
snapshot
2014-05-10
Ferruccio Guidi
advances on cofrees
commit
|
commitdiff
|
tree
|
snapshot
2014-04-27
Ferruccio Guidi
reordering abstract computation properties and saturati...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-25
Ferruccio Guidi
one file was missing ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-25
Ferruccio Guidi
- advances in the theory of cofrees
commit
|
commitdiff
|
tree
|
snapshot
2014-04-21
Ferruccio Guidi
- we introduce recursive free variables of a term in...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-20
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-20
Ferruccio Guidi
- name changes in the rediction rules
commit
|
commitdiff
|
tree
|
snapshot
2014-04-18
Ferruccio Guidi
update in basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-18
Ferruccio Guidi
- the relation for pointwise extensions now takes a...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-16
Ferruccio Guidi
anniversary milestone in basic_2 !!
commit
|
commitdiff
|
tree
|
snapshot
2014-04-16
Ferruccio Guidi
3rd anniversary milestone
commit
|
commitdiff
|
tree
|
snapshot
2014-04-15
Ferruccio Guidi
- lazy extended reduction parked
commit
|
commitdiff
|
tree
|
snapshot
2014-04-13
Ferruccio Guidi
we restored the strong normalization of extended comput...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-10
Ferruccio Guidi
commit completed: one file was missing :(
commit
|
commitdiff
|
tree
|
snapshot
2014-04-10
Ferruccio Guidi
- some work on extensions:
commit
|
commitdiff
|
tree
|
snapshot
2014-04-08
Ferruccio Guidi
some advances on pointwise union for local environments ...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-07
Ferruccio Guidi
some resuls on pointwise extensions (all of them are...
commit
|
commitdiff
|
tree
|
snapshot
2014-04-05
Ferruccio Guidi
commit completed:
commit
|
commitdiff
|
tree
|
snapshot
2014-04-02
Ferruccio Guidi
commit of the "computation" component with lazy pointwi...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-30
Ferruccio Guidi
update of the partial commit:
commit
|
commitdiff
|
tree
|
snapshot
2014-03-25
Ferruccio Guidi
- partial commit: just the components below "computation"
commit
|
commitdiff
|
tree
|
snapshot
2014-03-20
Ferruccio Guidi
continuing on lazy pointwise extensions ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-19
Ferruccio Guidi
we begin to develop lazy pointwisee extensions ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-11
Ferruccio Guidi
update in ground_2 and basic_2 ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-11
Ferruccio Guidi
reaxiomatized lleq fixes a bug in it and allows to...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-10
Ferruccio Guidi
some additions ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-08
Ferruccio Guidi
we define the lazy poinwise extension of a relation...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-08
Ferruccio Guidi
some corrections ...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Claudio Sacerdoti...
Code changed a bit to make it work as before with OCaml...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Claudio Sacerdoti...
Do not assert false for a print not implemented yet.
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Claudio Sacerdoti...
Hocus-pocus code to use the old (and deprecated) implem...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-07
Andrea Asperti
Minor changes to make the script more robust to strateg...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Ferruccio Guidi
some external links updated
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Ferruccio Guidi
a suggestion was added to avoid 1 pseudo reduction...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Claudio Sacerdoti...
Inclusions improved to allow compilation from the toplevel.
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Claudio Sacerdoti...
Bug fixed: the tactic to analyze the term and understan...
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Claudio Sacerdoti...
OCaml 4.0 detects a not handled case.
commit
|
commitdiff
|
tree
|
snapshot
2014-03-04
Claudio Sacerdoti...
Different behaviour of OCaml 4.0.
commit
|
commitdiff
|
tree
|
snapshot
2014-03-03
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-03-03
Ferruccio Guidi
some additions for the forthcoming presentation
commit
|
commitdiff
|
tree
|
snapshot
2014-02-28
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-28
Ferruccio Guidi
- some corrections and additions
commit
|
commitdiff
|
tree
|
snapshot
2014-02-27
Claudio Sacerdoti...
Porting of HOTT from Coq to Matita.
commit
|
commitdiff
|
tree
|
snapshot
2014-02-25
Ferruccio Guidi
relabelled documantation entries
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Ferruccio Guidi
update in web site and basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-24
Ferruccio Guidi
- we bypassed another false conjecture :) ...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-22
Ferruccio Guidi
addition of unused material :)
commit
|
commitdiff
|
tree
|
snapshot
2014-02-22
Ferruccio Guidi
update in ground_2 and basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-22
Ferruccio Guidi
a wrong conjecture bypassed!
commit
|
commitdiff
|
tree
|
snapshot
2014-02-21
Ferruccio Guidi
update in basic_2 and ground_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-21
Ferruccio Guidi
- main proposition on lsx finally proved!
commit
|
commitdiff
|
tree
|
snapshot
2014-02-18
Ferruccio Guidi
- a reinforement in a lemma on ldrop allows to prove...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-16
Ferruccio Guidi
- improved definition of lsx allows more invariants
commit
|
commitdiff
|
tree
|
snapshot
2014-02-11
Ferruccio Guidi
update in basic_2 and ground_2
commit
|
commitdiff
|
tree
|
snapshot
2014-02-11
Ferruccio Guidi
some advances on reduction
commit
|
commitdiff
|
tree
|
snapshot
2014-02-04
Ferruccio Guidi
evaluation for context-sensitive extended substitution...
commit
|
commitdiff
|
tree
|
snapshot
2014-02-03
Ferruccio Guidi
we start total substitution ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-31
Ferruccio Guidi
some notation renamed and fixed
commit
|
commitdiff
|
tree
|
snapshot
2014-01-30
Ferruccio Guidi
normal forms for extended substitution
commit
|
commitdiff
|
tree
|
snapshot
2014-01-29
Ferruccio Guidi
bug fix in the notation of normal forms, now we specify...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Andrea Asperti
Almost there
commit
|
commitdiff
|
tree
|
snapshot
2014-01-28
Andrea Asperti
progress
commit
|
commitdiff
|
tree
|
snapshot
2014-01-27
Ferruccio Guidi
some corrections ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-27
Andrea Asperti
working version
commit
|
commitdiff
|
tree
|
snapshot
2014-01-26
Ferruccio Guidi
nat: we added a non-indexed theorem
commit
|
commitdiff
|
tree
|
snapshot
2014-01-26
Andrea Asperti
more auxiliary machines
commit
|
commitdiff
|
tree
|
snapshot
2014-01-26
Ferruccio Guidi
- nat: some additions, plus_minus_commutative renamed...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-20
Ferruccio Guidi
milestone in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-01-20
Ferruccio Guidi
commit completed: now we support two versions of slicin...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-18
Ferruccio Guidi
- commit of the "reduction" component with two addition...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-17
Ferruccio Guidi
commit of the "unfold" component ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-17
Ferruccio Guidi
commit of the "static" component
commit
|
commitdiff
|
tree
|
snapshot
2014-01-17
Ferruccio Guidi
- commit of the "substitution" component
commit
|
commitdiff
|
tree
|
snapshot
2014-01-16
Ferruccio Guidi
commit of the "relocation" component with the new defin...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-15
Ferruccio Guidi
we start a criterion on extended computation
commit
|
commitdiff
|
tree
|
snapshot
2014-01-13
Ferruccio Guidi
some improvements on the relation lsx ...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-10
Ferruccio Guidi
update in ground_2 and basic_2
commit
|
commitdiff
|
tree
|
snapshot
2014-01-10
Ferruccio Guidi
new definition of lleq allows to complete the proof...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-09
Ferruccio Guidi
- ynat: some additions
commit
|
commitdiff
|
tree
|
snapshot
2014-01-06
Ferruccio Guidi
one file was missing :)
commit
|
commitdiff
|
tree
|
snapshot
2014-01-06
Ferruccio Guidi
- lleq now uses ynat
commit
|
commitdiff
|
tree
|
snapshot
2014-01-05
Ferruccio Guidi
- new definition of lazy equivalence for local environm...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-03
Ferruccio Guidi
- extended multiple substitutions now uses bounds in...
commit
|
commitdiff
|
tree
|
snapshot
2014-01-03
Ferruccio Guidi
more arithmetics for natural numbers with infinity ...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-28
Ferruccio Guidi
some improvements and new lemmas for
commit
|
commitdiff
|
tree
|
snapshot
2013-12-26
Ferruccio Guidi
the theory of extended multiple substitution for therms...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-20
Ferruccio Guidi
theory of extended iterated substitution begins ...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-19
Ferruccio Guidi
theory of cpy is complete!
commit
|
commitdiff
|
tree
|
snapshot
2013-12-19
Ferruccio Guidi
the theory of cpy continues ...
commit
|
commitdiff
|
tree
|
snapshot
2013-12-17
Ferruccio Guidi
refinement for extended substitution completed
commit
|
commitdiff
|
tree
|
snapshot
2013-12-16
Ferruccio Guidi
- lsubr moved down one component
commit
|
commitdiff
|
tree
|
snapshot
2013-12-15
Ferruccio Guidi
update in basic_2
commit
|
commitdiff
|
tree
|
snapshot
2013-12-15
Ferruccio Guidi
eliminators of arited terms based on "big tree" proper...
commit
|
commitdiff
|
tree
|
snapshot
next