]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/tptp_grafite/tptp2grafite.ml
fixed bug in coercion application, input/output swapped in unification
[helm.git] / helm / software / components / tptp_grafite / tptp2grafite.ml
2009-10-02 Enrico Tassifixed bug in coercion application, input/output swapped...
2009-07-28 Claudio Sacerdoti... Introduction of vectors of implicit (only for NG).
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces...
2009-06-22 denesSmall debugging in tptp2grafite
2009-06-18 Claudio Sacerdoti... 1) grafiteWalker removed
2009-06-15 Enrico Tassitacticals are really tactics now, they have an AST...
2009-06-12 Enrico Tassi-ng implemented
2009-06-05 Ferruccio Guidi- Procedural convertible rewrites in the conclusion...
2009-06-03 Claudio Sacerdoti... Huge commit with several changes:
2009-05-28 Ferruccio Guidi- cicInspect: relevant nodes count updated: letin nodes...
2009-05-19 Andrea AspertiNotEq is now considered as a negative Eq atom
2009-05-19 Enrico Tassifixed generation of horn clauses, negated atoms are...
2008-03-20 Enrico Tassichanged auto_tac params type and all derivate tactics...
2007-07-25 Enrico Tassi; and not . after auto-paramodulation
2007-07-19 Claudio Sacerdoti... map_unicode_to_tex is no longer optional and it always...
2007-05-24 Enrico Tassiauto and autogui... some work
2007-05-09 Ferruccio GuidiPrimitiveTactics: intros _ now aveilable
2007-04-20 Claudio Sacerdoti... Much ado about nothing:
2007-04-17 Enrico Tassiadded generation of hne and heq problems
2006-12-12 Ferruccio Guidiwe parametrized CicNotationPt.obj on 'term
2006-07-24 Enrico Tassiadded timeout parameter to auto paramodulation.
2006-07-22 Enrico Tassimatitaprover