| 2008-04-02 |
Enrico Tassi | added slim version of does_not_occur
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | added translation of Set to Type0 (avoid warning)
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | fixes backported from the new kernel
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrite
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrite
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | removed dummy rewrites
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | fixed according to the new rewrite semantics (fails...
|
commit | commitdiff | tree |
| 2008-04-02 |
Enrico Tassi | fixed depends after the removal of Fsub
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | better check for progress
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | progress made better, still not perfect
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | added to rewrite a check to effectively do something...
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | added some comments, but the samentics of many functions...
|
commit | commitdiff | tree |
| 2008-04-01 |
Enrico Tassi | added set_ppterm
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | more cases of the type checker honoured, still missing...
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | added is_closed to nCicUtils.
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | moved psubst and list to the new iterators, result...
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | added iterators over NCic terms
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | removed FSF header
|
commit | commitdiff | tree |
| 2008-03-27 |
Enrico Tassi | insert comments of old tpechecker
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | new are_convertible and head_beta_reduce
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | context for fixpoint body created in the hopefully...
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | ported to the Cic LetIn with explicit type
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | this patch is a shit, the part that fixes the heuristic...
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | fix with m (to be optimized) are rewritten such that...
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | very very interesting hack
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | argument of type mcu_type always abstracted first
|
commit | commitdiff | tree |
| 2008-03-25 |
Enrico Tassi | XXX this is the beginning of the metaocaml work XXX
|
commit | commitdiff | tree |
| 2008-03-23 |
Enrico Tassi | Fsub moved in contribs
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | since many stuff is under contrib, we need to ignore...
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | library_auto moved inside contrib, still not ported...
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | moved dama/ and dama_didactic/ in contribs/dama/
|
commit | commitdiff | tree |
| 2008-03-22 |
Enrico Tassi | freescale moved under contribs. contribs made relocatable
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | changed auto_tac params type and all derivate tactics...
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | new semantics for 'by t'
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | removed pointless test
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | I believe that auto paramodulation does not try to
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | added library option to auto
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | letins are no more unfolded, we do that by hand
|
commit | commitdiff | tree |
| 2008-03-20 |
Enrico Tassi | letin are no longer unfolded thus coercions not propagated...
|
commit | commitdiff | tree |
| 2008-03-12 |
Enrico Tassi | fixed implicit
|
commit | commitdiff | tree |
| 2008-03-12 |
Enrico Tassi | if -debug is specified do not catch all exceptions
|
commit | commitdiff | tree |
| 2008-03-10 |
Enrico Tassi | fixed wrong dependencies in debian package reported...
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | * please let the library in shape *
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | fixed
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | skipped freescale and dama_didactic
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | fixed deps
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | reworked freescale stuff to put \m as a left parameter
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | no more assembly/ to skip
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | fix typo
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | added mkdir
|
commit | commitdiff | tree |
| 2008-03-06 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-03-05 |
Enrico Tassi | from now on, export MATITA_EXTRACT=true to extract
|
commit | commitdiff | tree |
| 2008-03-05 |
Enrico Tassi | verbosity increased in case of error
|
commit | commitdiff | tree |
| 2008-02-28 |
Enrico Tassi | firs attempt to compile with ocamlbuild
|
commit | commitdiff | tree |
| 2008-02-20 |
Enrico Tassi | splat_args is now better understood and debugged: we...
|
commit | commitdiff | tree |
| 2008-02-20 |
Enrico Tassi | added small test, fixed some bugs
|
commit | commitdiff | tree |
| 2008-02-20 |
Enrico Tassi | many fixed in translation functions
|
commit | commitdiff | tree |
| 2008-02-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-02-19 |
Enrico Tassi | snapshot inverse tranformation
|
commit | commitdiff | tree |
| 2008-02-19 |
Enrico Tassi | transformation almost finisced, not tested
|
commit | commitdiff | tree |
| 2008-02-19 |
Enrico Tassi | initial steps of convertibility
|
commit | commitdiff | tree |
| 2008-02-18 |
Enrico Tassi | some bits of reduction, reusing psubst
|
commit | commitdiff | tree |
| 2008-02-13 |
Enrico Tassi | conversion half inplemented
|
commit | commitdiff | tree |
| 2008-02-13 |
Enrico Tassi | reordered cases
|
commit | commitdiff | tree |
| 2008-02-13 |
Enrico Tassi | reorganization of sources
|
commit | commitdiff | tree |
| 2008-02-13 |
Enrico Tassi | substituion and lifting implemented
|
commit | commitdiff | tree |
| 2008-02-13 |
Enrico Tassi | factorized common components of objects
|
commit | commitdiff | tree |
| 2008-02-13 |
Enrico Tassi | added Local pragma, moved leftno and inductive into...
|
commit | commitdiff | tree |
| 2008-02-13 |
Enrico Tassi | added leftno to indtypes, better indentation and comments
|
commit | commitdiff | tree |
| 2008-02-12 |
Enrico Tassi | nCic almost finished
|
commit | commitdiff | tree |
| 2008-02-12 |
Enrico Tassi | fixed path for matitadep
|
commit | commitdiff | tree |
| 2008-02-12 |
Enrico Tassi | fixed make dist
|
commit | commitdiff | tree |
| 2008-02-12 |
Enrico Tassi | better error message in case inclusion failed
|
commit | commitdiff | tree |
| 2008-02-12 |
Enrico Tassi | allow to use "../foo/bar.ma" as a path for the include...
|
commit | commitdiff | tree |
| 2008-02-05 |
Enrico Tassi | cic defined (half)
|
commit | commitdiff | tree |
| 2008-02-05 |
Enrico Tassi | reindent
|
commit | commitdiff | tree |
| 2008-02-05 |
Enrico Tassi | oldenv2newenv cache
|
commit | commitdiff | tree |
| 2008-02-05 |
Enrico Tassi | uri and references(uri)
|
commit | commitdiff | tree |
| 2008-02-05 |
Enrico Tassi | uri -> reference (2)
|
commit | commitdiff | tree |
| 2008-02-05 |
Enrico Tassi | uri -> reference
|
commit | commitdiff | tree |
| 2008-02-04 |
Enrico Tassi | sad snapshot
|
commit | commitdiff | tree |
| 2008-02-04 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2008-02-04 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2008-02-01 |
Enrico Tassi | very bad bug found, asert false in cicReduction when...
|
commit | commitdiff | tree |
| 2008-01-31 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2008-01-31 |
Enrico Tassi | new uri defined
|
commit | commitdiff | tree |
| 2008-01-31 |
Enrico Tassi | snapshot]
|
commit | commitdiff | tree |
| 2008-01-31 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2008-01-30 |
Enrico Tassi | added meta for the new kernel
|
commit | commitdiff | tree |
| 2008-01-30 |
Enrico Tassi | stub functions to make all compile
|
commit | commitdiff | tree |
| 2008-01-30 |
Enrico Tassi | basic organization of the new kernel
|
commit | commitdiff | tree |
| 2008-01-24 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-01-23 |
Enrico Tassi | snapshot with more duality, almost where we left without...
|
commit | commitdiff | tree |
| 2008-01-22 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2008-01-21 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2008-01-21 |
Enrico Tassi | snopshot before isabellization
|
commit | commitdiff | tree |
| 2008-01-16 |
Enrico Tassi | snapshot
|
commit | commitdiff | tree |
| 2008-01-16 |
Enrico Tassi | 3.27 ok
|
commit | commitdiff | tree |
| 2008-01-16 |
Enrico Tassi | yes! the lattice_(#) -> prelattice(<) -> lattice(<...
|
commit | commitdiff | tree |
| 2008-01-14 |
Enrico Tassi | more lemmas, til 3.26
|
commit | commitdiff | tree |
| next |
projects / helm.git / search