| 2010-03-31 |
Andrea Asperti | Tracing mechanism for auto. Interface changed to solve... |
tree | commitdiff |
| 2010-03-24 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-11-16 |
Wilmer Ricciotti | Implementation of ndestruct tactic (including destructi... |
tree | commitdiff |
| 2009-10-06 |
Wilmer Ricciotti | Inverters/Inversion: |
tree | commitdiff |
| 2009-10-05 |
Enrico Tassi | added auto_cache in the dupable status after an |
tree | commitdiff |
| 2009-10-02 |
Wilmer Ricciotti | Updated command ninverter. Syntax: |
tree | commitdiff |
| 2009-10-02 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-09-30 |
Wilmer Ricciotti | Added initial support for inversion principles in Matit... |
tree | commitdiff |
| 2009-09-09 |
Enrico Tassi | depends |
tree | commitdiff |
| 2009-07-07 |
Claudio Sacerdoti... | 1) Include files for NG were neither recursively proces... |
tree | commitdiff |
| 2009-06-25 |
Ferruccio Guidi | - some depend files :) |
tree | commitdiff |
| 2009-06-25 |
Enrico Tassi | initial import of standalone matitaprover binary |
tree | commitdiff |
| 2009-06-15 |
Enrico Tassi | huge commit regarding the grafite_status: |
tree | commitdiff |
| 2009-06-10 |
Ferruccio Guidi | - library/list/list.ma: unused code commented |
tree | commitdiff |
| 2009-06-03 |
Claudio Sacerdoti... | Huge commit with several changes: |
tree | commitdiff |
| 2009-05-27 |
Andrea Asperti | Avoiding to filter the application of congruence equations |
tree | commitdiff |
| 2009-05-25 |
Enrico Tassi | nasty change in the lexer/parser: |
tree | commitdiff |
| 2009-05-22 |
Andrea Asperti | Pruning candidates in the applicative case for equalities. |
tree | commitdiff |
| 2009-05-20 |
Andrea Asperti | Removed a silly type check |
tree | commitdiff |
| 2009-05-18 |
Enrico Tassi | nothing special |
tree | commitdiff |
| 2009-05-15 |
Claudio Sacerdoti... | Patch to add a debugging string to HExtlib.split_nth... |
tree | commitdiff |
| 2009-05-14 |
Ferruccio Guidi | - hExtlib: added debugging information for split_nth |
tree | commitdiff |
| 2009-05-13 |
Ferruccio Guidi | - matitaEngine: some commands like "coercion" must... |
tree | commitdiff |
| 2009-05-13 |
Andrea Asperti | The singature of the "by" universe is added to the... |
tree | commitdiff |
| 2009-05-13 |
Andrea Asperti | Signature is computed on the initial goal, once and... |
tree | commitdiff |
| 2009-05-12 |
Andrea Asperti | We only filter the smart candidates w.r.t the signature |
tree | commitdiff |
| 2009-05-08 |
Claudio Sacerdoti... | ... |
tree | commitdiff |
| 2009-05-08 |
Andrea Asperti | Constructors are closed with thier types when computing... |
tree | commitdiff |
| 2009-05-06 |
Enrico Tassi | apply and auto.equational_case call saturation.solve_na... |
tree | commitdiff |
| 2009-05-05 |
Andrea Asperti | Nuova gestione di "by" per auto. |
tree | commitdiff |
| 2009-04-30 |
Enrico Tassi | run check_if_goal_is_solved on all goals (active+passive) |
tree | commitdiff |
| 2009-04-30 |
Andrea Asperti | Added a passive table |
tree | commitdiff |
| 2009-04-30 |
Andrea Asperti | Calling paramodulation instead of demod_all |
tree | commitdiff |
| 2009-04-29 |
Enrico Tassi | call paramod instead of solve_Rewrite |
tree | commitdiff |
| 2009-04-29 |
Enrico Tassi | no typing |
tree | commitdiff |
| 2009-04-29 |
Enrico Tassi | many checks guarded with if Utils.debug_metas |
tree | commitdiff |
| 2009-04-28 |
Enrico Tassi | depenalization of smart apply inside auto, that is... |
tree | commitdiff |
| 2009-04-28 |
Enrico Tassi | fixed bug, demodulation was keeping results not strictl... |
tree | commitdiff |
| 2009-04-28 |
Enrico Tassi | huge commit in automation: |
tree | commitdiff |
| 2009-04-22 |
Wilmer Ricciotti | Disabled debug prints in the inversion principle. |
tree | commitdiff |
| 2009-04-22 |
Wilmer Ricciotti | New command "inverter" used to generate an induction... |
tree | commitdiff |
| 2009-04-22 |
Enrico Tassi | demodulate takes an extra argument 'all', if present... |
tree | commitdiff |
| 2009-04-21 |
Enrico Tassi | fixed last file restricting auto tables |
tree | commitdiff |
| 2009-04-20 |
Enrico Tassi | - init_cache_and_tables rewritten using the automation_... |
tree | commitdiff |
| 2009-04-16 |
Enrico Tassi | Universe is used only locally to tactics/ |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | we rebuilt the dependences |
tree | commitdiff |
| 2009-04-14 |
Ferruccio Guidi | - Procedural: generation of "exact" is now complete |
tree | commitdiff |
| 2009-03-25 |
Enrico Tassi | new tactics are almost ready |
tree | commitdiff |
| 2009-03-16 |
Andrea Asperti | New parameters for applyS: 10 20. |
tree | commitdiff |
| 2009-03-10 |
Andrea Asperti | A version of applyS with bounded iterations of given_cl... |
tree | commitdiff |
| 2009-03-10 |
Andrea Asperti | Removed the context from the metasenv to avoid trivial... |
tree | commitdiff |
| 2009-02-15 |
Enrico Tassi | commented some printings |
tree | commitdiff |
| 2009-02-12 |
Andrea Asperti | errata corrige. |
tree | commitdiff |
| 2009-02-12 |
Andrea Asperti | Fixed a problem of lifting. |
tree | commitdiff |
| 2009-02-03 |
Enrico Tassi | case tactic first tries with a simple outtype and then... |
tree | commitdiff |
| 2009-01-15 |
Enrico Tassi | - name mangling changed, added __ to separate additiona... |
tree | commitdiff |
| 2009-01-13 |
Enrico Tassi | many changes regarding coercions: |
tree | commitdiff |
| 2009-01-08 |
Enrico Tassi | more composites to make all happy! |
tree | commitdiff |
| 2008-11-27 |
Enrico Tassi | 1. grafiteDisambiguator => multiPassDisambiguator |
tree | commitdiff |
| 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 |
| next |
projects / helm.git / history