projects
/
helm.git
/ shortlog
commit
grep
author
committer
pickaxe
?
search:
re
summary
| shortlog |
log
|
commit
|
commitdiff
|
tree
first ⋅ prev ⋅
next
helm.git
2009-06-23
denes
Fixed nasty bug in maxvar updating
commit
|
commitdiff
|
tree
|
snapshot
2009-06-23
Claudio Sacerdoti...
- Bug fixed: removed URIs were not removed from the...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-23
Enrico Tassi
removed problem not in UEQ
commit
|
commitdiff
|
tree
|
snapshot
2009-06-22
Ferruccio Guidi
- nodes count is now working for aut and meta
commit
|
commitdiff
|
tree
|
snapshot
2009-06-22
denes
Added more precise time information
commit
|
commitdiff
|
tree
|
snapshot
2009-06-22
denes
Added problems from CASC 208
commit
|
commitdiff
|
tree
|
snapshot
2009-06-22
denes
Regenerated problems with corrected tptp2grafite
commit
|
commitdiff
|
tree
|
snapshot
2009-06-22
denes
Corrected proof visiting (topological sort)
commit
|
commitdiff
|
tree
|
snapshot
2009-06-22
denes
Small debugging in tptp2grafite
commit
|
commitdiff
|
tree
|
snapshot
2009-06-21
Wilmer Ricciotti
Added injective compose
commit
|
commitdiff
|
tree
|
snapshot
2009-06-21
Ferruccio Guidi
- cicNotationPp: bugfix in record syntax
commit
|
commitdiff
|
tree
|
snapshot
2009-06-20
Wilmer Ricciotti
Some notation and additional lemmata.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-20
Claudio Sacerdoti...
Debugging
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
"matitaclean all" ported to NG
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
Invert dependencies between baseuris (files) are now...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
Bug fixed: refreshing of uris for the db.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Wilmer Ricciotti
More improvements.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
The global db is now updated during decompilation.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
Persistent db (to lookup names in the library) ineffici...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
NG decompilation is now activated. However, it is calle...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
Estatus finally merged into the global status using...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
Useless GrafiteTypes.get_baseuri removed.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
More statuses converted to objects.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-19
Claudio Sacerdoti...
Good:
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
Enrico Tassi
debug pps removed
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
Enrico Tassi
better exception handling
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
Enrico Tassi
proof patching!
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
Claudio Sacerdoti...
Objects are now used to represent also the tactic status.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
denes
Added ntry and nassumption tactics
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
Enrico Tassi
callbacks were taking in input a status bu were not...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
denes
Fixed stupid path
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
denes
Added script useful for running benchmarks
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
denes
Changed parenthesis to optional around letin ident...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
denes
Fixed wrong types in proof terms
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
Claudio Sacerdoti...
Stricter type: the type now shows that disambiguation...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-18
Claudio Sacerdoti...
1) grafiteWalker removed
commit
|
commitdiff
|
tree
|
snapshot
2009-06-17
Enrico Tassi
proof reconstruction almost OK
commit
|
commitdiff
|
tree
|
snapshot
2009-06-17
Claudio Sacerdoti...
Initial implementation of statuses using objects in...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-17
denes
Added optionnal one pass simplification (instead of...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Enrico Tassi
first proof reconstruction attempt, still bugged since it
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Claudio Sacerdoti...
1) unification hint now takes NG terms (as it should...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Claudio Sacerdoti...
1) NCicLibrary (which is untrusted) moved after NCicUnt...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Claudio Sacerdoti...
Implementation of existential type improved (more stric...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Enrico Tassi
avoid fixing non-recursive terms
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Enrico Tassi
we fix recursive object reference with the correct...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Claudio Sacerdoti...
FIX OF THE PREVIOUS EXPERIMENTAL COMMIT:
commit
|
commitdiff
|
tree
|
snapshot
2009-06-16
Ferruccio Guidi
we corrected some reduction bugs about renaming.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Ferruccio Guidi
we removed some old code and fixed a reduction bug...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Enrico Tassi
EXPERIMENTAL COMMIT (part B, by CSC :-):
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Enrico Tassi
EXPERIMENTAL COMMIT (by CSC,actuall :-)
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Enrico Tassi
added TODO list
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Enrico Tassi
huge commit regarding the grafite_status:
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Enrico Tassi
part of last commit
commit
|
commitdiff
|
tree
|
snapshot
2009-06-15
Enrico Tassi
tacticals are really tactics now, they have an AST...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-13
Ferruccio Guidi
we removed some coercion detours and we added some...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-12
denes
Implemented keep_simplified.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-12
Claudio Sacerdoti...
ocaml sucks...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-12
Claudio Sacerdoti...
...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-12
Enrico Tassi
-ng implemented
commit
|
commitdiff
|
tree
|
snapshot
2009-06-12
Andrea Asperti
Added a new keep_simplified function
commit
|
commitdiff
|
tree
|
snapshot
2009-06-12
Andrea Asperti
Renamed forward_simplify into simplify and backward_sim...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-11
denes
Active goals are now demodulated after selecting a...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-11
Ferruccio Guidi
- applyTransformation: bugfix in the rendering of records
commit
|
commitdiff
|
tree
|
snapshot
2009-06-11
Enrico Tassi
content2pres for the new cic fixed
commit
|
commitdiff
|
tree
|
snapshot
2009-06-11
Ferruccio Guidi
- some depend files fixed
commit
|
commitdiff
|
tree
|
snapshot
2009-06-10
Ferruccio Guidi
- library/list/list.ma: unused code commented
commit
|
commitdiff
|
tree
|
snapshot
2009-06-10
Enrico Tassi
1) added simplification of actives w.r.t. selected
commit
|
commitdiff
|
tree
|
snapshot
2009-06-10
Enrico Tassi
right inference step completed
commit
|
commitdiff
|
tree
|
snapshot
2009-06-10
Enrico Tassi
new function filter_map_acc
commit
|
commitdiff
|
tree
|
snapshot
2009-06-10
denes
Extended the equality case to non ground terms
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Ferruccio Guidi
- Procedural: more support for the Debug inline option...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Claudio Sacerdoti...
Debugging code removed.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Claudio Sacerdoti...
Temporary (and partially broken) patch for Ferruccio...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
almost complete superposition right step
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
snapshot
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
see the previous commit
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
termAcicContent is logic independent (despite its name...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
denes
Optimized weigths comparison, removed normalization
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
snaphost: supright almost done
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
denes
Implemented substitution application and concatenation
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
fixed metas
commit
|
commitdiff
|
tree
|
snapshot
2009-06-09
Enrico Tassi
fixed building
commit
|
commitdiff
|
tree
|
snapshot
2009-06-08
Enrico Tassi
...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-08
Enrico Tassi
a skeleton of supright
commit
|
commitdiff
|
tree
|
snapshot
2009-06-08
Enrico Tassi
some more functors and a nice higher-order all_position...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-08
Enrico Tassi
added META for ng_paramodulation
commit
|
commitdiff
|
tree
|
snapshot
2009-06-06
Claudio Sacerdoti...
Previous commit reverted, as explained in that log.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-06
Claudio Sacerdoti...
This commit restores the ids_to_father_ids table.
commit
|
commitdiff
|
tree
|
snapshot
2009-06-06
Enrico Tassi
some renaming to make ocamlopt happy
commit
|
commitdiff
|
tree
|
snapshot
2009-06-05
Ferruccio Guidi
bugfix in Include syntax: it was changed and committed...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-05
Ferruccio Guidi
- Procedural convertible rewrites in the conclusion...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-05
denes
First tests for paramodulation (pretty printer, unifica...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-05
Wilmer Ricciotti
- replaced part1a/defn with the version based on induct...
commit
|
commitdiff
|
tree
|
snapshot
2009-06-05
denes
Fix : wrong exception was catch in apply_subst
commit
|
commitdiff
|
tree
|
snapshot
2009-06-05
Claudio Sacerdoti...
1) the home button of CicBrowser now works also for NG
commit
|
commitdiff
|
tree
|
snapshot
2009-06-05
Claudio Sacerdoti...
The kernel _must_ check the correctness of the height...
commit
|
commitdiff
|
tree
|
snapshot
next