| 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 |
| 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 |
| next |
projects / helm.git / history