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 |
2007-06-30 |
Claudio Sacerdoti... | BU Conversion was not generated for Rels fixed. I wonde... |
tree | commitdiff |
2007-06-30 |
Claudio Sacerdoti... | Nicer layout but possibly more bugged. |
tree | commitdiff |
2007-06-30 |
Claudio Sacerdoti... | Spurious "we need to prove" at the beginning of Intros... |
tree | commitdiff |
2007-06-23 |
Enrico Tassi | removed ugly printings |
tree | commitdiff |
2007-06-14 |
Claudio Sacerdoti... | Incompatible syntax problem between MySql e Sqlite3... |
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-06-01 |
Enrico Tassi | hacks for paramodulation declarative proofs |
tree | commitdiff |
2007-05-31 |
Claudio Sacerdoti... | DOOMSDAY 1.0: |
tree | commitdiff |
2007-05-31 |
Claudio Sacerdoti... | Bug fixed: wrong id. |
tree | commitdiff |
2007-05-31 |
Claudio Sacerdoti... | Ferruccio has changed the semantics of the old ~pattern... |
tree | commitdiff |
2007-05-29 |
Enrico Tassi | hSqlite3.ml used create_fun_2 to define REGEXP. |
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-24 |
Enrico Tassi | fixed a when that was causing backtrace loss |
tree | commitdiff |
2007-05-24 |
Enrico Tassi | added some flags to render subproofs (an hack) |
tree | commitdiff |
next |