| 2010-03-31 |
Andrea Asperti | Tracing mechanism for auto. Interface changed to solve... |
blob | commitdiff | raw |
| 2009-05-27 |
Andrea Asperti | Avoiding to filter the application of congruence equations |
blob | commitdiff | raw | diff to current |
| 2009-05-22 |
Andrea Asperti | Pruning candidates in the applicative case for equalities. |
blob | commitdiff | raw | diff to current |
| 2009-05-13 |
Andrea Asperti | The singature of the "by" universe is added to the... |
blob | commitdiff | raw | diff to current |
| 2009-05-13 |
Andrea Asperti | Signature is computed on the initial goal, once and... |
blob | commitdiff | raw | diff to current |
| 2009-05-12 |
Andrea Asperti | We only filter the smart candidates w.r.t the signature |
blob | commitdiff | raw | diff to current |
| 2009-05-06 |
Enrico Tassi | apply and auto.equational_case call saturation.solve_na... |
blob | commitdiff | raw | diff to current |
| 2009-05-05 |
Andrea Asperti | Nuova gestione di "by" per auto. |
blob | commitdiff | raw | diff to current |
| 2009-04-30 |
Andrea Asperti | Calling paramodulation instead of demod_all |
blob | commitdiff | raw | diff to current |
| 2009-04-29 |
Enrico Tassi | call paramod instead of solve_Rewrite |
blob | commitdiff | raw | diff to current |
| 2009-04-28 |
Enrico Tassi | depenalization of smart apply inside auto, that is... |
blob | commitdiff | raw | diff to current |
| 2009-04-28 |
Enrico Tassi | huge commit in automation: |
blob | commitdiff | raw | diff to current |
| 2009-04-22 |
Enrico Tassi | demodulate takes an extra argument 'all', if present... |
blob | commitdiff | raw | diff to current |
| 2009-04-21 |
Enrico Tassi | fixed last file restricting auto tables |
blob | commitdiff | raw | diff to current |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
blob | commitdiff | raw | diff to current |
| 2009-04-16 |
Enrico Tassi | Universe is used only locally to tactics/ |
blob | commitdiff | raw | diff to current |
| 2009-03-16 |
Andrea Asperti | New parameters for applyS: 10 20. |
blob | commitdiff | raw | diff to current |
| 2009-03-10 |
Andrea Asperti | A version of applyS with bounded iterations of given_cl... |
blob | commitdiff | raw | diff to current |
| 2008-11-16 |
Enrico Tassi | removed some printings |
blob | commitdiff | raw | diff to current |
| 2008-11-07 |
Andrea Asperti | debug=false |
blob | commitdiff | raw | diff to current |
| 2008-11-07 |
Andrea Asperti | The signature in "retrieve equations" must be extended... |
blob | commitdiff | raw | diff to current |
| 2008-11-05 |
Enrico Tassi | new internal flags for auto: |
blob | commitdiff | raw | diff to current |
| 2008-11-03 |
Enrico Tassi | removed prerr_endline |
blob | commitdiff | raw | diff to current |
| 2008-11-03 |
Enrico Tassi | debug=false |
blob | commitdiff | raw | diff to current |
| 2008-11-01 |
Enrico Tassi | added lazy |
blob | commitdiff | raw | diff to current |
| 2008-10-29 |
Andrea Asperti | Propagation of changes in paramodulation. |
blob | commitdiff | raw | diff to current |
| 2008-09-26 |
Enrico Tassi | auto was compiraing lazy proof terms with = ... fixed |
blob | commitdiff | raw | diff to current |
| 2008-09-26 |
Enrico Tassi | lazy proof term to increase sharing and decrease memory... |
blob | commitdiff | raw | diff to current |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
blob | commitdiff | raw | diff to current |
| 2008-05-24 |
Enrico Tassi | order of goals changes, open ones are preferred to... |
blob | commitdiff | raw | diff to current |
| 2008-04-22 |
Enrico Tassi | oblivion ugraph everywhere outside the kernel |
blob | commitdiff | raw | diff to current |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics... |
blob | commitdiff | raw | diff to current |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
blob | commitdiff | raw | diff to current |
| 2007-12-04 |
Enrico Tassi | if parameter type is given, this assert is false |
blob | commitdiff | raw | diff to current |
| 2007-11-17 |
Enrico Tassi | moved to pkg-ocaml-maint |
blob | commitdiff | raw | diff to current |
| 2007-11-15 |
Enrico Tassi | removed ugly prerr_endline |
blob | commitdiff | raw | diff to current |
| 2007-08-23 |
Claudio Sacerdoti... | Bug fixed: the initial metasenv used in the two tactic... |
blob | commitdiff | raw | diff to current |
| 2007-06-13 |
Enrico Tassi | many changes: |
blob | commitdiff | raw | diff to current |
| 2007-06-06 |
Enrico Tassi | sort_new_elems on prop_only |
blob | commitdiff | raw | diff to current |
| 2007-05-29 |
Enrico Tassi | added some lines to compile for debugging |
blob | commitdiff | raw | diff to current |
| 2007-05-29 |
Enrico Tassi | added pruning option in autogui |
blob | commitdiff | raw | diff to current |
| 2007-05-29 |
Andrea Asperti | Corrected version od meta_convertibnility_subst. |
blob | commitdiff | raw | diff to current |
| 2007-05-28 |
Claudio Sacerdoti... | Bug fixed (hopefully without introducing new ones)... |
blob | commitdiff | raw | diff to current |
| 2007-05-28 |
Andrea Asperti | Improved pruning (no propress). |
blob | commitdiff | raw | diff to current |
| 2007-05-25 |
Enrico Tassi | added $Revision$ |
blob | commitdiff | raw | diff to current |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
blob | commitdiff | raw | diff to current |
| 2007-05-18 |
lzingare | added alternative implementation for hMysql relying |
blob | commitdiff | raw | diff to current |
| 2007-05-17 |
Enrico Tassi | added a (for the moment) dummy field _subst to Proofeng... |
blob | commitdiff | raw | diff to current |
| 2007-05-17 |
Enrico Tassi | auto rewritten with only one tail recursive function. |
blob | commitdiff | raw | diff to current |
| 2007-05-07 |
Enrico Tassi | ... |
blob | commitdiff | raw | diff to current |
| 2007-05-07 |
Enrico Tassi | some minor fixes done in cividale (bugfix coming from... |
blob | commitdiff | raw | diff to current |
| 2007-04-30 |
Andrea Asperti | Even if we are at depth 0, we first check in the cache... |
blob | commitdiff | raw | diff to current |
| 2007-04-30 |
Andrea Asperti | Removed an assert false; everything works again, but... |
blob | commitdiff | raw | diff to current |
| 2007-04-27 |
Andrea Asperti | Subst is passed in input to apapluy, so no need to... |
blob | commitdiff | raw | diff to current |
| 2007-02-09 |
Claudio Sacerdoti... | Debugging code fixed. To enable debugging just set... |
blob | commitdiff | raw | diff to current |
| 2007-01-10 |
Ferruccio Guidi | attributes now in the proof status: commit 2 |
blob | commitdiff | raw | diff to current |
| 2006-12-29 |
Ferruccio Guidi | - tactics: |
blob | commitdiff | raw | diff to current |
| 2006-12-14 |
Claudio Sacerdoti... | Huge commit: |
blob | commitdiff | raw | diff to current |
| 2006-11-29 |
Andrea Asperti | Demodulate_tac now depends on the universe |
blob | commitdiff | raw | diff to current |
| 2006-11-27 |
Andrea Asperti | Only modified for taking unfold into account. |
blob | commitdiff | raw | diff to current |
| 2006-11-23 |
Andrea Asperti | Modifications to auto due to the introduction of the... |
blob | commitdiff | raw | diff to current |
| 2006-10-25 |
Andrea Asperti | Added a couple of flags to auto |
blob | commitdiff | raw | diff to current |
| 2006-10-20 |
Andrea Asperti | Major changes to auto, documented on the helm mailing... |
blob | commitdiff | raw | diff to current |
| 2006-10-12 |
Enrico Tassi | timeout if unspecfied should be set to infinity, not... |
blob | commitdiff | raw | diff to current |
| 2006-10-12 |
Claudio Sacerdoti... | The default for paramodulation is now back to false... |
blob | commitdiff | raw | diff to current |
| 2006-10-11 |
Claudio Sacerdoti... | My previous commit changed the regular timeout of param... |
blob | commitdiff | raw | diff to current |
| 2006-10-09 |
Claudio Sacerdoti... | 1. applyS now uses its ~params |
blob | commitdiff | raw | diff to current |
| 2006-10-09 |
Claudio Sacerdoti... | applyS now receives the same parameters that auto receives. |
blob | commitdiff | raw | diff to current |
| 2006-10-03 |
Andrea Asperti | Changed auto from implicit to option and renamed a... |
blob | commitdiff | raw | diff to current |
| 2006-10-02 |
Enrico Tassi | 50 steps on goal are fine for irrat2 |
blob | commitdiff | raw | diff to current |
| 2006-09-29 |
Enrico Tassi | new version of auto that is able to prove the irrationa... |
blob | commitdiff | raw | diff to current |
| 2006-09-27 |
Enrico Tassi | auto snapshot |
blob | commitdiff | raw | diff to current |
| 2006-09-21 |
Enrico Tassi | auto snapshot |
blob | commitdiff | raw | diff to current |
|
projects / helm.git / history