| 2007-10-26 |
Enrico Tassi | we use ulex08 not ulex
|
commit | commitdiff | tree |
| 2007-10-22 |
Enrico Tassi | fixed copyright file... an ITP should be done
|
commit | commitdiff | tree |
| 2007-10-16 |
Enrico Tassi | fixed make opt
|
commit | commitdiff | tree |
| 2007-10-09 |
Enrico Tassi | added patch to allow i,j,k: skip and *: skip
|
commit | commitdiff | tree |
| 2007-09-19 |
Enrico Tassi | commented out pack coercion, since the code is not...
|
commit | commitdiff | tree |
| 2007-09-14 |
Enrico Tassi | since compat <> 3 no cmx* in the install.in bu just cm*
|
commit | commitdiff | tree |
| 2007-09-11 |
Enrico Tassi | replaced an assert false that cause nat_ind not to...
|
commit | commitdiff | tree |
| 2007-09-10 |
Enrico Tassi | last version with caml 3.09 built and saved as 0.3.0
|
commit | commitdiff | tree |
| 2007-09-10 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-09-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-09-09 |
Enrico Tassi | in the case of coerce_to_sort the whd was done with...
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | huge commit regarding coercions to funclass and eat_prods...
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | the order of abstraction is now correct, but there...
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | removed an assertion that makes no more sense to me
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | better debug printings
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | better test for church numerals
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | just a Pcre expression fixed, nothing real
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | matita can now safely start a matitac that will put...
|
commit | commitdiff | tree |
| 2007-09-08 |
Enrico Tassi | Full specification of find. Added notation for If_Then_Else...
|
commit | commitdiff | tree |
| 2007-09-07 |
Enrico Tassi | 1. fix_arity fixed: the code is totally wrong and this...
|
commit | commitdiff | tree |
| 2007-09-07 |
Enrico Tassi | This cast now works!
|
commit | commitdiff | tree |
| 2007-09-07 |
Enrico Tassi | when a coercion is passed through a case on right-params...
|
commit | commitdiff | tree |
| 2007-09-07 |
Enrico Tassi | ooops, missing )
|
commit | commitdiff | tree |
| 2007-09-07 |
Enrico Tassi | disabled coercions when refining paramod proofs (attemt...
|
commit | commitdiff | tree |
| 2007-09-07 |
Enrico Tassi | fixed propagation under Fix/Lambda/Case of coercions...
|
commit | commitdiff | tree |
| 2007-09-06 |
Enrico Tassi | coercions under Fix and Case. Code refactoring needed
|
commit | commitdiff | tree |
| 2007-09-06 |
Enrico Tassi | added a duplicated implementation of replace lifting
|
commit | commitdiff | tree |
| 2007-09-06 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-08-31 |
Enrico Tassi | fixed coercions between arrows when the arrow is dependent.
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | captured exception preserved (was replaced blindly...
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | reverted assertion, since it may happen to look for...
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | refactoring of all coercions code and add a check to...
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | bugfix in computation of src and tgt for coercions...
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | tests for coercions under lambdas
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | Coercions rework:
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | coercions from funclass are not supported
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | bla bla bla fallback
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | added a binch of svn:ignore
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | add a fallback in case the binaries are in the path...
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | print few more wired assertions
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | the version on the livecd
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | more stuff to reach an intensional definition of finite...
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | added an utility function
|
commit | commitdiff | tree |
| 2007-08-30 |
Enrico Tassi | 0.2.0
|
commit | commitdiff | tree |
| 2007-07-31 |
Enrico Tassi | something was really too slow...
|
commit | commitdiff | tree |
| 2007-07-31 |
Enrico Tassi | default equality stuff filtered out from hint rewrite
|
commit | commitdiff | tree |
| 2007-07-31 |
Enrico Tassi | removed comments in proof presentation
|
commit | commitdiff | tree |
| 2007-07-30 |
Enrico Tassi | added 'rewrite' option to the the hint macro. a cicBrowser...
|
commit | commitdiff | tree |
| 2007-07-26 |
Enrico Tassi | added development path normalization, inclusions with...
|
commit | commitdiff | tree |
| 2007-07-26 |
Enrico Tassi | auto -> autobatch
|
commit | commitdiff | tree |
| 2007-07-26 |
Enrico Tassi | more stuff about coercions
|
commit | commitdiff | tree |
| 2007-07-26 |
Enrico Tassi | little bug in coercion generation found. it use to...
|
commit | commitdiff | tree |
| 2007-07-25 |
Enrico Tassi | added some notation
|
commit | commitdiff | tree |
| 2007-07-25 |
Enrico Tassi | added another example in which our coercions are powerful
|
commit | commitdiff | tree |
| 2007-07-25 |
Enrico Tassi | used ;try assumption instead of .try assumption
|
commit | commitdiff | tree |
| 2007-07-25 |
Enrico Tassi | ; and not . after auto-paramodulation
|
commit | commitdiff | tree |
| 2007-07-25 |
Enrico Tassi | reverted previous fix
|
commit | commitdiff | tree |
| 2007-07-25 |
Enrico Tassi | restored compaction of metas at the end of given_clause
|
commit | commitdiff | tree |
| 2007-07-24 |
Enrico Tassi | added test about dependent coercions
|
commit | commitdiff | tree |
| 2007-07-23 |
Enrico Tassi | fixed makefiles to make it compile cleanly again
|
commit | commitdiff | tree |
| 2007-07-19 |
Enrico Tassi | COERCIONS: tentative addition of an equivalence relation...
|
commit | commitdiff | tree |
| 2007-07-19 |
Enrico Tassi | the cade was escaping the table name and not the uri
|
commit | commitdiff | tree |
| 2007-07-19 |
Enrico Tassi | fixed escaping for sqlite
|
commit | commitdiff | tree |
| 2007-07-19 |
Enrico Tassi | fixed an escaping error, added more infos to the generic...
|
commit | commitdiff | tree |
| 2007-07-18 |
Enrico Tassi | recursive argument in let rec is not printed explicitly.
|
commit | commitdiff | tree |
| 2007-07-18 |
Enrico Tassi | fixed coercion graph print, moved coercion graph and...
|
commit | commitdiff | tree |
| 2007-07-17 |
Enrico Tassi | fixed includes and added notation for bytes
|
commit | commitdiff | tree |
| 2007-07-10 |
Enrico Tassi | La programmazione funzionale e' come TeX, funziona...
|
commit | commitdiff | tree |
| 2007-07-10 |
Enrico Tassi | fixed a bug in the cleanup ofsedir that was not properly...
|
commit | commitdiff | tree |
| 2007-07-10 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-07-09 |
Enrico Tassi | 1. bug fixed in tick
|
commit | commitdiff | tree |
| 2007-07-09 |
Enrico Tassi | signal hadler restored after runnig external 'make'
|
commit | commitdiff | tree |
| 2007-07-09 |
Enrico Tassi | added few more fun to this test
|
commit | commitdiff | tree |
| 2007-07-09 |
Enrico Tassi | auto->autobatch
|
commit | commitdiff | tree |
| 2007-07-07 |
Enrico Tassi | inclusion of div_and_mod
|
commit | commitdiff | tree |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs.
|
commit | commitdiff | tree |
| 2007-06-23 |
Enrico Tassi | removed ugly printings
|
commit | commitdiff | tree |
| 2007-06-21 |
Enrico Tassi | better description
|
commit | commitdiff | tree |
| 2007-06-21 |
Enrico Tassi | better description
|
commit | commitdiff | tree |
| 2007-06-21 |
Enrico Tassi | here we are, a version that compiles and seems to run
|
commit | commitdiff | tree |
| 2007-06-13 |
Enrico Tassi | cut is now implemented building a letin and not a beta...
|
commit | commitdiff | tree |
| 2007-06-13 |
Enrico Tassi | many changes:
|
commit | commitdiff | tree |
| 2007-06-06 |
Enrico Tassi | sort_new_elems on prop_only
|
commit | commitdiff | tree |
| 2007-06-06 |
Enrico Tassi | fixed to allow make-dist
|
commit | commitdiff | tree |
| 2007-06-06 |
Enrico Tassi | added doc for compose
|
commit | commitdiff | tree |
| 2007-06-06 |
Enrico Tassi | compose now returns a good metasenv
|
commit | commitdiff | tree |
| 2007-06-04 |
Enrico Tassi | tentative fix
|
commit | commitdiff | tree |
| 2007-06-04 |
Enrico Tassi | auto proof are printed in procedural style
|
commit | commitdiff | tree |
| 2007-06-04 |
Enrico Tassi | new more flexible compose, see matita/tests/compose...
|
commit | commitdiff | tree |
| 2007-06-02 |
Enrico Tassi | wrong assertion was inserted, now just a warning to...
|
commit | commitdiff | tree |
| 2007-06-01 |
Enrico Tassi | removed some refinement_toolkit
|
commit | commitdiff | tree |
| 2007-06-01 |
Enrico Tassi | new compose tactic, still undocumented.
|
commit | commitdiff | tree |
| 2007-06-01 |
Enrico Tassi | hacks for paramodulation declarative proofs
|
commit | commitdiff | tree |
| 2007-05-30 |
Enrico Tassi | now the window can be closed also using X
|
commit | commitdiff | tree |
| 2007-05-29 |
Enrico Tassi | hSqlite3.ml used create_fun_2 to define REGEXP.
|
commit | commitdiff | tree |
| 2007-05-29 |
Enrico Tassi | added some lines to compile for debugging
|
commit | commitdiff | tree |
| 2007-05-29 |
Enrico Tassi | added pruning option in autogui
|
commit | commitdiff | tree |
| 2007-05-25 |
Enrico Tassi | added $Revision$
|
commit | commitdiff | tree |
| next |
projects / helm.git / search