| 2007-11-02 |
Claudio Sacerdoti... | *** Very experimental and not branched *** |
tree | commitdiff |
| 2007-11-02 |
Ferruccio Guidi | - tacticals: new tactical ifs added: uses thens where... |
tree | commitdiff |
| 2007-11-02 |
Claudio Sacerdoti... | Added an hook useful in many situations. |
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 | ... |
tree | commitdiff |
| 2007-10-26 |
Enrico Tassi | rebuilt |
tree | commitdiff |
| 2007-10-26 |
Enrico Tassi | rebuilt |
tree | commitdiff |
| 2007-10-26 |
Claudio Sacerdoti... | Syntax of patterns changed (and not documented yet). |
tree | commitdiff |
| 2007-10-26 |
Claudio Sacerdoti... | Wildcard patterns implemented in case analysis. The... |
tree | commitdiff |
| 2007-10-25 |
Ferruccio Guidi | bug fix in injection e relocate term |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Ooops. In previous commit I forgot to subtract the... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: case analysis where a case had not the expec... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: a MutCase considering a wrong number of... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: a MutCase with missing or exceeding cases... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | 1. More localization: interpretation errors are now... |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Recently introduced bug fixed: error localization was... |
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 |
Claudio Sacerdoti... | Debugging code improved. |
tree | commitdiff |
| 2007-10-24 |
Ferruccio Guidi | - new function for general relocation of local referenc... |
tree | commitdiff |
| 2007-10-16 |
Enrico Tassi | fixed make opt |
tree | commitdiff |
| 2007-10-16 |
Claudio Sacerdoti... | DOS-style CR+LF added to the blanks list. |
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-23 |
Ferruccio Guidi | we chmod the created directories to override the umask... |
tree | commitdiff |
| 2007-09-23 |
Ferruccio Guidi | fixed some file permissions (anybody can rebuild a... |
tree | commitdiff |
| 2007-09-19 |
Enrico Tassi | commented out pack coercion, since the code is not... |
tree | commitdiff |
| 2007-09-11 |
Ferruccio Guidi | librarySync - we do not generate the object attributes... |
tree | commitdiff |
| 2007-09-11 |
Enrico Tassi | replaced an assert false that cause nat_ind not to... |
tree | commitdiff |
| 2007-09-09 |
Enrico Tassi | in the case of coerce_to_sort the whd was done with... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | huge commit regarding coercions to funclass and eat_pro... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | the order of abstraction is now correct, but there... |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | removed an assertion that makes no more sense to me |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | better debug printings |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | just a Pcre expression fixed, nothing real |
tree | commitdiff |
| 2007-09-08 |
Enrico Tassi | matita can now safely start a matitac that will put... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | 1. fix_arity fixed: the code is totally wrong and this... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | when a coercion is passed through a case on right-param... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | ooops, missing ) |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | disabled coercions when refining paramod proofs (attemt... |
tree | commitdiff |
| 2007-09-07 |
Enrico Tassi | fixed propagation under Fix/Lambda/Case of coercions... |
tree | commitdiff |
| 2007-09-06 |
Enrico Tassi | coercions under Fix and Case. Code refactoring needed |
tree | commitdiff |
| 2007-09-06 |
Enrico Tassi | added a duplicated implementation of replace lifting |
tree | commitdiff |
| 2007-09-05 |
Ferruccio Guidi | - lybrarySync: |
tree | commitdiff |
| 2007-09-05 |
Claudio Sacerdoti... | coercions are propagated under Fix (but not mutually... |
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-31 |
Enrico Tassi | fixed coercions between arrows when the arrow is dependent. |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | captured exception preserved (was replaced blindly... |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | reverted assertion, since it may happen to look for... |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | refactoring of all coercions code and add a check to... |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | bugfix in computation of src and tgt for coercions... |
tree | commitdiff |
| 2007-08-30 |
Claudio Sacerdoti... | Coercions are now generalized to the general form |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | Coercions rework: |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | coercions from funclass are not supported |
tree | commitdiff |
| 2007-08-30 |
Enrico Tassi | added an utility function |
tree | commitdiff |
| 2007-08-23 |
Claudio Sacerdoti... | Bug fixed: RewriteLR were not recognized correctly... |
tree | commitdiff |
| 2007-08-23 |
Claudio Sacerdoti... | Bug fixed: the initial metasenv used in the two tactic... |
tree | commitdiff |
| 2007-08-22 |
Claudio Sacerdoti... | Avoid reusing Hbeta several times. |
tree | commitdiff |
| 2007-08-22 |
Claudio Sacerdoti... | select now works correctly even if multiple hypotheses... |
tree | commitdiff |
| 2007-08-21 |
Claudio Sacerdoti... | Avoid confusion for names of proofs put in the applicat... |
tree | commitdiff |
| 2007-08-21 |
Claudio Sacerdoti... | "obtain H E1=E2 by proof" is now working |
tree | commitdiff |
| 2007-07-31 |
Enrico Tassi | removed comments in proof presentation |
tree | commitdiff |
| 2007-07-30 |
Enrico Tassi | added 'rewrite' option to the the hint macro. a cicBrow... |
tree | commitdiff |
| 2007-07-26 |
Ferruccio Guidi | We add a binary for computing the "heights" of helm... |
tree | commitdiff |
| 2007-07-26 |
Enrico Tassi | little bug in coercion generation found. it use to... |
tree | commitdiff |
| 2007-07-25 |
Enrico Tassi | ; and not . after auto-paramodulation |
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-22 |
Ferruccio Guidi | Procedural: the statement body and it inner types must... |
tree | commitdiff |
| 2007-07-20 |
Ferruccio Guidi | acic_procedural: bug fix: |
tree | commitdiff |
| 2007-07-20 |
Claudio Sacerdoti... | Tentative bug fix for diverging pretty-printing function. |
tree | commitdiff |
| 2007-07-19 |
Ferruccio Guidi | cicUtil : new test function "is_sober" to test... |
tree | commitdiff |
| 2007-07-19 |
Claudio Sacerdoti... | Convertibility now converts machines in place of terms. |
tree | commitdiff |
| 2007-07-19 |
Claudio Sacerdoti... | map_unicode_to_tex is no longer optional and it always... |
tree | commitdiff |
| 2007-07-19 |
Enrico Tassi | COERCIONS: tentative addition of an equivalence relatio... |
tree | commitdiff |
| 2007-07-19 |
Enrico Tassi | the cade was escaping the table name and not the uri |
tree | commitdiff |
| 2007-07-19 |
Enrico Tassi | fixed escaping for sqlite |
tree | commitdiff |
| 2007-07-19 |
Enrico Tassi | fixed an escaping error, added more infos to the generi... |
tree | commitdiff |
| 2007-07-18 |
Ferruccio Guidi | the predicate for elim was not built correctly when... |
tree | commitdiff |
| 2007-07-18 |
Enrico Tassi | recursive argument in let rec is not printed explicitly. |
tree | commitdiff |
| 2007-07-13 |
Claudio Sacerdoti... | Dirty patch by Zack: natural numbers of Matita are... |
tree | commitdiff |
| 2007-07-11 |
Ferruccio Guidi | native dependences fixed |
tree | commitdiff |
| 2007-07-10 |
Claudio Sacerdoti... | New reduction strategy: the new reduction strategy... |
tree | commitdiff |
| 2007-07-10 |
Ferruccio Guidi | persistent inner types are now generated in publishing... |
tree | commitdiff |
| 2007-07-10 |
Enrico Tassi | fixed a bug in the cleanup ofsedir that was not properl... |
tree | commitdiff |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | Quick hack: matita natural numbers are now accepted... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | Bug fixed: a ~with_cast is now inserted when appropriat... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | In place of conclude, obtain FIXMEXXX is now generated... |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | 1. Code simplification |
tree | commitdiff |
| 2007-07-04 |
Claudio Sacerdoti... | is_top_down was not propageted correctly under a bottom... |
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-07-04 |
Claudio Sacerdoti... | Bug fixed: name in letin was printed as "previous"... |
tree | commitdiff |
| 2007-06-30 |
Claudio Sacerdoti... | In order to generate executable declarative scripts... |
tree | commitdiff |
| 2007-06-30 |
Claudio Sacerdoti... | Bug fixed in bottom-up conversion. |
tree | commitdiff |
| next |
projects / helm.git / history