projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2007-11-14
Enrico Tassi
ogroups almost finished
commit
|
commitdiff
|
tree
|
snapshot
2007-11-14
Enrico Tassi
snapshot
commit
|
commitdiff
|
tree
|
snapshot
2007-11-14
Enrico Tassi
snapshot
commit
|
commitdiff
|
tree
|
snapshot
2007-11-13
Enrico Tassi
End of groups :-)
commit
|
commitdiff
|
tree
|
snapshot
2007-11-13
Enrico Tassi
snapshot
commit
|
commitdiff
|
tree
|
snapshot
2007-11-13
Ferruccio Guidi
- ProofEngineHelpers: namer_of moved to GrafiteEngine
commit
|
commitdiff
|
tree
|
snapshot
2007-11-13
Ferruccio Guidi
previously hidden simplifications (in old destruct...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
some work till the need of redoing all groups based...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
since there is no more tab, the modification of the...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Ferruccio Guidi
- destruct tactic: automatic simplification in case...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
removed ugly printing
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
ordered_sets are built with excedence
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
added ordered sets
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
renamed ordered sets into excedence.ma
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
relocated
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
removed dust
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
HIDDEN (since glade do not read out file properly anymo...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
new file with some relations stated in Type
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Enrico Tassi
ordered set is over, much new stuff coming from a coref...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-12
Ferruccio Guidi
refactoring
commit
|
commitdiff
|
tree
|
snapshot
2007-11-10
Ferruccio Guidi
old subst tactics removed. New destruct tactic used...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-10
Claudio Sacerdoti...
a) Detection of existential types now implemented
commit
|
commitdiff
|
tree
|
snapshot
2007-11-10
Claudio Sacerdoti...
More correct (but still bugged) implementation of type...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-10
Claudio Sacerdoti...
Dead code removed.
commit
|
commitdiff
|
tree
|
snapshot
2007-11-09
Enrico Tassi
snapshot
commit
|
commitdiff
|
tree
|
snapshot
2007-11-09
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Ferruccio Guidi
- subst tactic keyword removed from highlight syntax...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Claudio Sacerdoti...
Trivial bug fixed in type inference of LetIn source...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Enrico Tassi
xxx
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Enrico Tassi
ported to the new destruct
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Claudio Sacerdoti...
Arguments of constructors in a case pattern are now...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Claudio Sacerdoti...
svn:ignore set
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Enrico Tassi
please, commit files with debug=false otherwise the...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Enrico Tassi
forced associativity in if construct
commit
|
commitdiff
|
tree
|
snapshot
2007-11-08
Claudio Sacerdoti...
Zoli's note (in Italian) about a constructive version...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-07
Ferruccio Guidi
set svn:ignore to *.ml in the deve directories
commit
|
commitdiff
|
tree
|
snapshot
2007-11-07
Ferruccio Guidi
- bug fix in destruct
commit
|
commitdiff
|
tree
|
snapshot
2007-11-07
Enrico Tassi
reorganization of the whole story, the root dir contain...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-07
Enrico Tassi
Code extraction unbranched again.
commit
|
commitdiff
|
tree
|
snapshot
2007-11-06
Ferruccio Guidi
new implementation of the destruct tactic,
commit
|
commitdiff
|
tree
|
snapshot
2007-11-06
Claudio Sacerdoti...
cic_acic should be compiled before cic_exportation
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
Bug in detection of too polymorphic types partially...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
MutCases that occur in types should be handled with...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
Obj.magic are now generated to extract dependently...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
Handling of left parameters of constructors/indutive...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
Slightly nicer output.
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
Filenames are now fully mangled (e.g. matita_nat_nat...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
Type application and abstractions are now exported...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
New OCaml keyword "val".
commit
|
commitdiff
|
tree
|
snapshot
2007-11-05
Claudio Sacerdoti...
"f" => "aux" to avoid name clashes
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
The type parameters in an inductive type declaration...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
Type arguments are better uncapitalized.
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
Empty types not in Prop and empty types elimination...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
Empty and singleton type elimination are now handled...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
1. type definitions of propositions are no longer expor...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
Bug fixed: qualified names were not generated correctly...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
* type definitions that define a new proposition are...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
CicExportation branched. Change "if false" with "if...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
All exported names are now qualified. This avoids the...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-04
Claudio Sacerdoti...
All names are now qualified. This avoids the need for...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-02
Claudio Sacerdoti...
*** Very experimental and not branched ***
commit
|
commitdiff
|
tree
|
snapshot
2007-11-02
Ferruccio Guidi
- tacticals: new tactical ifs added: uses thens where...
commit
|
commitdiff
|
tree
|
snapshot
2007-11-02
Claudio Sacerdoti...
Added an hook useful in many situations.
commit
|
commitdiff
|
tree
|
snapshot
2007-11-02
Enrico Tassi
finisced configuration section
commit
|
commitdiff
|
tree
|
snapshot
2007-11-02
Enrico Tassi
added doc for db and getter sections
commit
|
commitdiff
|
tree
|
snapshot
2007-11-02
Enrico Tassi
added notes about sqlite and removed obsolete zack...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-31
Claudio Sacerdoti...
New image from Tassi's PhD thesis.
commit
|
commitdiff
|
tree
|
snapshot
2007-10-30
Ferruccio Guidi
better implementation of if_
commit
|
commitdiff
|
tree
|
snapshot
2007-10-30
Enrico Tassi
remade dependencies that were wrong
commit
|
commitdiff
|
tree
|
snapshot
2007-10-29
Ferruccio Guidi
- destruct: core of subst tactic implemented,
commit
|
commitdiff
|
tree
|
snapshot
2007-10-29
Ferruccio Guidi
reverted matita db configuration fixed
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Claudio Sacerdoti...
Bug fixed: patterns in hypotheses under binders where...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Claudio Sacerdoti...
New syntax for match patterns in terms and in patterns.
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Claudio Sacerdoti...
The document was not valid. Fixed.
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Claudio Sacerdoti...
Pretty-printing of "match ... with" pattern syntax...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Claudio Sacerdoti...
Nil => nil, Cons => cons
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Claudio Sacerdoti...
Nil => nil; Cons => cons
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Claudio Sacerdoti...
New syntax for match patterns.
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Enrico Tassi
clean can't fail
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Enrico Tassi
added patch for the configuration file
commit
|
commitdiff
|
tree
|
snapshot
2007-10-28
Enrico Tassi
reverted last commit
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Enrico Tassi
rebuilt
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Enrico Tassi
no -rectype passed to ocamldep
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Enrico Tassi
rebuilt
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Enrico Tassi
0.4.0 almost working
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Claudio Sacerdoti...
Syntax of patterns changed (and not documented yet).
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Claudio Sacerdoti...
Wildcard patterns implemented in case analysis. The...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-26
Enrico Tassi
we use ulex08 not ulex
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Ferruccio Guidi
bug fix in injection e relocate term
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
neg => Qneg :-)
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
true and false were swapped!
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
flase => false :-)
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
Ooops. In previous commit I forgot to subtract the...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
Bug fixed: case analysis where a case had not the expec...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
Bug fixed: a MutCase considering a wrong number of...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
Bug fixed: a MutCase with missing or exceeding cases...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
1. More localization: interpretation errors are now...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-25
Claudio Sacerdoti...
Recently introduced bug fixed: error localization was...
commit
|
commitdiff
|
tree
|
snapshot
2007-10-24
Ferruccio Guidi
bug fix in injection: we have to recur on the generated...
commit
|
commitdiff
|
tree
|
snapshot
next