| 2007-11-12 |
Enrico Tassi | since there is no more tab, the modification of the...
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | removed ugly printing
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | ordered_sets are built with excedence
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | added ordered sets
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | renamed ordered sets into excedence.ma
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | relocated
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | removed dust
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | HIDDEN (since glade do not read out file properly anymore...
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | new file with some relations stated in Type
|
commit | commitdiff | tree |
| 2007-11-12 |
Enrico Tassi | ordered set is over, much new stuff coming from a coreflexiv...
|
commit | commitdiff | tree |
| 2007-11-09 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2007-11-09 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-11-08 |
Enrico Tassi | xxx
|
commit | commitdiff | tree |
| 2007-11-08 |
Enrico Tassi | ported to the new destruct
|
commit | commitdiff | tree |
| 2007-11-08 |
Enrico Tassi | please, commit files with debug=false otherwise the...
|
commit | commitdiff | tree |
| 2007-11-08 |
Enrico Tassi | forced associativity in if construct
|
commit | commitdiff | tree |
| 2007-11-07 |
Enrico Tassi | reorganization of the whole story, the root dir contains...
|
commit | commitdiff | tree |
| 2007-11-07 |
Enrico Tassi | Code extraction unbranched again.
|
commit | commitdiff | tree |
| 2007-11-02 |
Enrico Tassi | finisced configuration section
|
commit | commitdiff | tree |
| 2007-11-02 |
Enrico Tassi | added doc for db and getter sections
|
commit | commitdiff | tree |
| 2007-11-02 |
Enrico Tassi | added notes about sqlite and removed obsolete zack...
|
commit | commitdiff | tree |
| 2007-10-30 |
Enrico Tassi | remade dependencies that were wrong
|
commit | commitdiff | tree |
| 2007-10-28 |
Enrico Tassi | clean can't fail
|
commit | commitdiff | tree |
| 2007-10-28 |
Enrico Tassi | added patch for the configuration file
|
commit | commitdiff | tree |
| 2007-10-28 |
Enrico Tassi | reverted last commit
|
commit | commitdiff | tree |
| 2007-10-26 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2007-10-26 |
Enrico Tassi | rebuilt
|
commit | commitdiff | tree |
| 2007-10-26 |
Enrico Tassi | no -rectype passed to ocamldep
|
commit | commitdiff | tree |
| 2007-10-26 |
Enrico Tassi | rebuilt
|
commit | commitdiff | tree |
| 2007-10-26 |
Enrico Tassi | 0.4.0 almost working
|
commit | commitdiff | tree |
| 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 |
| next |
projects / helm.git / search