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 |
2007-05-23 |
Claudio Sacerdoti... | Yet another patch to LibraryClean. |
tree | commitdiff |
2007-05-23 |
Claudio Sacerdoti... | HSql.Error ==> HSql.Error of string |
tree | commitdiff |
2007-05-23 |
Claudio Sacerdoti... | prerr_endine ==> debug_print everywhere |
tree | commitdiff |
2007-05-23 |
Claudio Sacerdoti... | Reindented. |
tree | commitdiff |
2007-05-23 |
Enrico Tassi | makefile reworked to make debian package possible |
tree | commitdiff |
2007-05-23 |
Enrico Tassi | changed the way environment variable can interfere... |
tree | commitdiff |
2007-05-23 |
Enrico Tassi | added is_writabledir to extlib |
tree | commitdiff |
2007-05-23 |
Enrico Tassi | added some hacks for the debian package |
tree | commitdiff |
2007-05-22 |
Claudio Sacerdoti... | Slightly more efficient patch. |
tree | commitdiff |
2007-05-20 |
Ferruccio Guidi | applyTransformation: added debugging information |
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-15 |
Ferruccio Guidi | more informations on nodes, fixed a bug on conversion... |
tree | commitdiff |
2007-05-15 |
Ferruccio Guidi | Wrong invariant: Hypothesis (i.e. lambda-abstractions... |
tree | commitdiff |
2007-05-14 |
Ferruccio Guidi | CSC: terrific bug fixed. Enrico commented the applicati... |
tree | commitdiff |
2007-05-13 |
Ferruccio Guidi | CicInspect: a function for counting the nodes of a... |
tree | commitdiff |
2007-05-10 |
Ferruccio Guidi | Procedural: clear tactics added |
tree | commitdiff |
2007-05-09 |
Ferruccio Guidi | PrimitiveTactics: intros _ now aveilable |
tree | commitdiff |
2007-05-08 |
Ferruccio Guidi | DoubleTypeInference: added a comment on "does_not_occur" |
tree | commitdiff |
2007-05-07 |
Enrico Tassi | ... |
tree | commitdiff |
2007-05-07 |
Enrico Tassi | a bit of sharing and the optimization of not folding... |
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-29 |
Ferruccio Guidi | GrafiteAstPp: \n's finally fixed |
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 | procedural: bug fixes |
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-24 |
Andrea Asperti | @ |
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 |
Enrico Tassi | developments root are now part of default inclusion... |
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-17 |
Enrico Tassi | added generation of hne and heq problems |
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-12 |
Enrico Tassi | HACK for indtype checking |
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 |
next |