| 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 |
| 2007-06-04 |
Enrico Tassi | new more flexible compose, see matita/tests/compose... |
tree | commitdiff |
| 2007-06-02 |
Enrico Tassi | wrong assertion was inserted, now just a warning to... |
tree | commitdiff |
| 2007-06-01 |
Enrico Tassi | removed some refinement_toolkit |
tree | commitdiff |
| 2007-06-01 |
Enrico Tassi | new compose tactic, still undocumented. |
tree | commitdiff |
| 2007-05-31 |
Claudio Sacerdoti... | Ferruccio has changed the semantics of the old ~pattern... |
tree | commitdiff |
| 2007-05-29 |
Enrico Tassi | added some lines to compile for debugging |
tree | commitdiff |
| 2007-05-29 |
Enrico Tassi | added pruning option in autogui |
tree | commitdiff |
| 2007-05-29 |
Andrea Asperti | Corrected version od meta_convertibnility_subst. |
tree | commitdiff |
| 2007-05-28 |
Claudio Sacerdoti... | Bug fixed (hopefully without introducing new ones)... |
tree | commitdiff |
| 2007-05-28 |
Andrea Asperti | Improved pruning (no propress). |
tree | commitdiff |
| 2007-05-28 |
Andrea Asperti | Added a new version of meta_convertibnility that return... |
tree | commitdiff |
| 2007-05-25 |
Enrico Tassi | added $Revision$ |
tree | commitdiff |
| 2007-05-24 |
Enrico Tassi | auto and autogui... some work |
tree | commitdiff |
| 2007-05-23 |
Claudio Sacerdoti... | prerr_endine ==> debug_print everywhere |
tree | commitdiff |
| 2007-05-18 |
Ferruccio Guidi | - new devel contribs/LAMBDA-TYPES/Base-2 with the autom... |
tree | commitdiff |
| 2007-05-18 |
lzingare | added alternative implementation for hMysql relying |
tree | commitdiff |
| 2007-05-18 |
Claudio Sacerdoti... | In some cases (e.g. JM equality) the inversion principl... |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | added a (for the moment) dummy field _subst to Proofeng... |
tree | commitdiff |
| 2007-05-17 |
Enrico Tassi | auto rewritten with only one tail recursive function. |
tree | commitdiff |
| 2007-05-09 |
Ferruccio Guidi | PrimitiveTactics: intros _ now aveilable |
tree | commitdiff |
| 2007-05-07 |
Enrico Tassi | ... |
tree | commitdiff |
| 2007-05-07 |
Enrico Tassi | some minor fixes done in cividale (bugfix coming from... |
tree | commitdiff |
| 2007-05-03 |
Ferruccio Guidi | elim with a pattern now works correctly (hopefully) |
tree | commitdiff |
| 2007-05-01 |
Ferruccio Guidi | SubstTactic: bug fix |
tree | commitdiff |
| 2007-04-30 |
Andrea Asperti | Even if we are at depth 0, we first check in the cache... |
tree | commitdiff |
| 2007-04-30 |
Andrea Asperti | Removed an assert false; everything works again, but... |
tree | commitdiff |
| 2007-04-28 |
Ferruccio Guidi | AMBDA-TYPES: some improvements. subst now fully exploited |
tree | commitdiff |
| 2007-04-27 |
Andrea Asperti | Subst is passed in input to apapluy, so no need to... |
tree | commitdiff |
| 2007-04-27 |
Andrea Asperti | Apply_with_subst now returns a subst with a correct... |
tree | commitdiff |
| 2007-04-26 |
Ferruccio Guidi | bug fix in subst tactic |
tree | commitdiff |
| 2007-04-24 |
Andrea Asperti | Subsumption_subst re-added to initial. |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | The declarative rewriting step now tries auto timeout... |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | Much ado about nothing: |
tree | commitdiff |
| 2007-04-20 |
Claudio Sacerdoti... | Interface of the argument to Continuationals.Make great... |
tree | commitdiff |
| 2007-04-19 |
Claudio Sacerdoti... | EXPERIMENTAL and _INCOMPLETE_ COMMIT: |
tree | commitdiff |
| 2007-04-18 |
Enrico Tassi | handles failures (sometimes you can't inject) |
tree | commitdiff |
| 2007-04-17 |
Enrico Tassi | one more step toward a decent destruct |
tree | commitdiff |
| 2007-04-17 |
Enrico Tassi | fixed a list.nth called on a too short list |
tree | commitdiff |
| 2007-04-16 |
Enrico Tassi | simplify has a brand new semantics! |
tree | commitdiff |
| 2007-04-16 |
Ferruccio Guidi | subst tactic put in a file on its own |
tree | commitdiff |
| 2007-04-10 |
Enrico Tassi | fixed case |
tree | commitdiff |
| 2007-04-10 |
Enrico Tassi | still not completely working but at least non dumb... |
tree | commitdiff |
| 2007-04-10 |
Enrico Tassi | you can case even if only a right appears... so, substi... |
tree | commitdiff |
| 2007-04-04 |
Ferruccio Guidi | alpha equivalence test factorized and moved to CicUtil |
tree | commitdiff |
| 2007-04-03 |
Enrico Tassi | new case implementation |
tree | commitdiff |
| 2007-04-02 |
Enrico Tassi | hopefully fixed cases implementation |
tree | commitdiff |
| 2007-03-22 |
Claudio Sacerdoti... | Several instances of the same bug fixed at once: when... |
tree | commitdiff |
| 2007-03-22 |
Claudio Sacerdoti... | Debugging code removed. |
tree | commitdiff |
| 2007-03-16 |
Ferruccio Guidi | elim tactic: it needs two arguments, a term as well... |
tree | commitdiff |
| 2007-03-13 |
Claudio Sacerdoti... | Role of |
tree | commitdiff |
| 2007-03-13 |
Ferruccio Guidi | elim tactic: now takes a pattern instead of just a... |
tree | commitdiff |
| 2007-03-10 |
Ferruccio Guidi | rewrite tactic: bug fix in rewriting under Pi's: |
tree | commitdiff |
| 2007-03-01 |
Ferruccio Guidi | Procedural: some improvements |
tree | commitdiff |
| 2007-03-01 |
Enrico Zoli | "by j let x : T such that P(x)" generalized to allow... |
tree | commitdiff |
| 2007-02-27 |
Ferruccio Guidi | - Procedural: some improvements |
tree | commitdiff |
| 2007-02-26 |
Ferruccio Guidi | decompose: delta-expansion of the type to eliminate... |
tree | commitdiff |
| 2007-02-25 |
Ferruccio Guidi | RELATIONAL: new undecomposable definition of NLE |
tree | commitdiff |
| 2007-02-21 |
Ferruccio Guidi | procedural : some improvements. |
tree | commitdiff |
| next |
projects / helm.git / history