| 2008-11-16 |
Enrico Tassi | removed some printings |
tree | commitdiff |
| 2008-11-16 |
Enrico Tassi | removed some printings |
tree | commitdiff |
| 2008-11-07 |
Andrea Asperti | debug=false |
tree | commitdiff |
| 2008-11-07 |
Andrea Asperti | Signature_of has been closed with respect to constructors. |
tree | commitdiff |
| 2008-11-07 |
Andrea Asperti | The signature in "retrieve equations" must be extended... |
tree | commitdiff |
| 2008-11-06 |
Enrico Tassi | the passive set and passive list are expected to have... |
tree | commitdiff |
| 2008-11-05 |
Enrico Tassi | new internal flags for auto: |
tree | commitdiff |
| 2008-11-05 |
Enrico Tassi | duplicate entry in menv avoided |
tree | commitdiff |
| 2008-11-04 |
Andrea Asperti | Calling unification instead of matching when checking... |
tree | commitdiff |
| 2008-11-03 |
Enrico Tassi | removed prerr_endline |
tree | commitdiff |
| 2008-11-03 |
Enrico Tassi | debug=false |
tree | commitdiff |
| 2008-11-01 |
Enrico Tassi | added lazy |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Propagation of changes in paramodulation. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Exported a couple of functions. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Added a in_universe function |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | propagation of changes in other paramodulation files. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | New demod function working for arbitary goals. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Enforcing the disjoint invariant between metasenvs. |
tree | commitdiff |
| 2008-10-29 |
Andrea Asperti | Main change: added a parameter to build_equality_proof... |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | auto was compiraing lazy proof terms with = ... fixed |
tree | commitdiff |
| 2008-09-26 |
Enrico Tassi | lazy proof term to increase sharing and decrease memory... |
tree | commitdiff |
| 2008-09-19 |
Enrico Tassi | more abstract discrimination tree |
tree | commitdiff |
| 2008-09-19 |
Enrico Tassi | better abstraction to allow 1 discrimination tree imple... |
tree | commitdiff |
| 2008-09-19 |
Enrico Tassi | Revised discrimination tree implementation: |
tree | commitdiff |
| 2008-09-19 |
Andrea Asperti | A temporary patch to demodulation theorem. |
tree | commitdiff |
| 2008-09-09 |
Enrico Tassi | some work to make tries "printable", fixed comparison... |
tree | commitdiff |
| 2008-08-28 |
Ferruccio Guidi | cicDischarge: new module for discharging the explicit... |
tree | commitdiff |
| 2008-07-07 |
Enrico Tassi | simplified coercDb implementation with additional info... |
tree | commitdiff |
| 2008-07-04 |
Ferruccio Guidi | - Procedural: bug fix in rendering the application... |
tree | commitdiff |
| 2008-07-02 |
Ferruccio Guidi | - new tactic applyP for use in the *P*rocedural script... |
tree | commitdiff |
| 2008-07-02 |
Enrico Tassi | calculation of the sort user to choose the rewriting... |
tree | commitdiff |
| 2008-06-19 |
Claudio Sacerdoti... | 1. bug fixed in generalize_pattern: a lazy const_tac... |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | Bug fixed: wrong default pattern for generalize. |
tree | commitdiff |
| 2008-06-08 |
Claudio Sacerdoti... | Hypotheses patterns for elim implemented. No more need... |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | new, more rigid syntax, for auto_params affecting the... |
tree | commitdiff |
| 2008-05-26 |
Enrico Tassi | Universe.key was not used to index terms, but was used... |
tree | commitdiff |
| 2008-05-24 |
Enrico Tassi | order of goals changes, open ones are preferred to... |
tree | commitdiff |
| 2008-04-22 |
Enrico Tassi | oblivion ugraph everywhere outside the kernel |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | better check for progress |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | progress made better, still not perfect |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | added to rewrite a check to effectively do something... |
tree | commitdiff |
| 2008-04-01 |
Enrico Tassi | added some comments, but the samentics of many function... |
tree | commitdiff |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
tree | commitdiff |
| 2008-03-19 |
Claudio Sacerdoti... | prerr_endline => debug_print |
tree | commitdiff |
| 2008-03-12 |
Enrico Tassi | fixed implicit |
tree | commitdiff |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Bad hack to avoid failure of conversion (unfolding... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Tactic reduce got rid of. Use normalize, instead. |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | An unimplemented case of clearbody is now implemented. |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Performance improvement: let-ins should always be pushe... |
tree | commitdiff |
| 2008-01-10 |
Enrico Tassi | BIG FAT WARNING: DEVELOPMENTS DIE HERE |
tree | commitdiff |
| 2007-12-04 |
Enrico Tassi | if parameter type is given, this assert is false |
tree | commitdiff |
| 2007-11-17 |
Enrico Tassi | moved to pkg-ocaml-maint |
tree | commitdiff |
| 2007-11-16 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-11-16 |
Enrico Tassi | compose tactic restore and added nocomposites keyword |
tree | commitdiff |
| 2007-11-15 |
Enrico Tassi | removed ugly prerr_endline |
tree | commitdiff |
| 2007-11-14 |
Ferruccio Guidi | now destruct takes an optional list of term rather... |
tree | commitdiff |
| 2007-11-13 |
Ferruccio Guidi | - ProofEngineHelpers: namer_of moved to GrafiteEngine |
tree | commitdiff |
| 2007-11-12 |
Ferruccio Guidi | - destruct tactic: automatic simplification in case... |
tree | commitdiff |
| 2007-11-08 |
Enrico Tassi | please, commit files with debug=false otherwise the... |
tree | commitdiff |
| 2007-11-07 |
Ferruccio Guidi | - bug fix in destruct |
tree | commitdiff |
| 2007-11-06 |
Ferruccio Guidi | new implementation of the destruct tactic, |
tree | commitdiff |
| 2007-11-04 |
Claudio Sacerdoti... | All exported names are now qualified. This avoids the... |
tree | commitdiff |
| 2007-11-02 |
Ferruccio Guidi | - tacticals: new tactical ifs added: uses thens where... |
tree | commitdiff |
| 2007-10-30 |
Ferruccio Guidi | better implementation of if_ |
tree | commitdiff |
| 2007-10-29 |
Ferruccio Guidi | - destruct: core of subst tactic implemented, |
tree | commitdiff |
| 2007-10-28 |
Claudio Sacerdoti... | Pretty-printing of "match ... with" pattern syntax... |
tree | commitdiff |
| 2007-10-26 |
Enrico Tassi | rebuilt |
tree | commitdiff |
| 2007-10-25 |
Ferruccio Guidi | bug fix in injection e relocate term |
tree | commitdiff |
| 2007-10-24 |
Ferruccio Guidi | bug fix in injection: we have to recur on the generated... |
tree | commitdiff |
| 2007-10-24 |
Ferruccio Guidi | we revisited the implementation of the destruct tactic... |
tree | commitdiff |
| 2007-10-24 |
Ferruccio Guidi | - new function for general relocation of local referenc... |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-10-11 |
Claudio Sacerdoti... | Old inversion bug fixed: it used to work only on the... |
tree | commitdiff |
| 2007-10-09 |
Enrico Tassi | added patch to allow i,j,k: skip and *: skip |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | the order of abstraction is now correct, but there... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | just a Pcre expression fixed, nothing real |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | disabled coercions when refining paramod proofs (attemt... |
tree | commitdiff |
| 2007-09-04 |
Claudio Sacerdoti... | Composition of coercions with arity > 0 is now implemen... |
tree | commitdiff |
| 2007-09-04 |
Claudio Sacerdoti... | 1. composition of coercions with saturations > 0 is... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-08-23 |
Claudio Sacerdoti... | Bug fixed: the initial metasenv used in the two tactic... |
tree | commitdiff |
| 2007-08-22 |
Claudio Sacerdoti... | select now works correctly even if multiple hypotheses... |
tree | commitdiff |
| 2007-08-21 |
Claudio Sacerdoti... | "obtain H E1=E2 by proof" is now working |
tree | commitdiff |
| 2007-07-26 |
Enrico Tassi | little bug in coercion generation found. it use to... |
tree | commitdiff |
| 2007-07-25 |
Enrico Tassi | reverted previous fix |
tree | commitdiff |
| 2007-07-25 |
Enrico Tassi | restored compaction of metas at the end of given_clause |
tree | commitdiff |
| 2007-07-20 |
Ferruccio Guidi | acic_procedural: bug fix: |
tree | commitdiff |
| 2007-07-19 |
Enrico Tassi | COERCIONS: tentative addition of an equivalence relatio... |
tree | commitdiff |
| 2007-07-18 |
Ferruccio Guidi | the predicate for elim was not built correctly when... |
tree | commitdiff |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | Bug fixed: a ~with_cast is now inserted when appropriat... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | 1. "by proof" now allowed as a justification in equalit... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | Added ~with_cast to the change tactic. |
tree | commitdiff |
| 2007-06-13 |
Enrico Tassi | cut is now implemented building a letin and not a beta... |
tree | commitdiff |
| 2007-06-13 |
Enrico Tassi | many changes: |
tree | commitdiff |
| 2007-06-06 |
Enrico Tassi | sort_new_elems on prop_only |
tree | commitdiff |
| 2007-06-06 |
Enrico Tassi | compose now returns a good metasenv |
tree | commitdiff |
| next |
projects / helm.git / history