| 2011-10-17 |
Enrico Tassi | compact coercion command: "coercion foo."
|
commit | commitdiff | tree |
| 2011-05-26 |
Enrico Tassi | Prod indexed as Dead, that is equal only to itself...
|
commit | commitdiff | tree |
| 2011-01-11 |
Enrico Tassi | ctrl+pgUp/Down to navigate tabs
|
commit | commitdiff | tree |
| 2011-01-11 |
Enrico Tassi | ctrl+pgUp/Down to navigate tabs
|
commit | commitdiff | tree |
| 2011-01-11 |
Enrico Tassi | coercion lookup now returns coercions ranked using...
|
commit | commitdiff | tree |
| 2011-01-07 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2011-01-07 |
Enrico Tassi | added retrieval function with weight
|
commit | commitdiff | tree |
| 2011-01-07 |
Enrico Tassi | non uniform coercion names in sync with the TYPES talk...
|
commit | commitdiff | tree |
| 2011-01-07 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-11-03 |
Enrico Tassi | notation kind of works
|
commit | commitdiff | tree |
| 2010-11-02 |
Enrico Tassi | big change in parsing, trying to make all functional
|
commit | commitdiff | tree |
| 2010-10-26 |
Enrico Tassi | add some virtuals
|
commit | commitdiff | tree |
| 2010-10-26 |
Enrico Tassi | fix queries
|
commit | commitdiff | tree |
| 2010-10-22 |
Enrico Tassi | tentative parser patch with symbolic tactics names
|
commit | commitdiff | tree |
| 2010-10-19 |
Enrico Tassi | camlp5 probably changed some internal data structures...
|
commit | commitdiff | tree |
| 2010-10-17 |
Enrico Tassi | fixed many scripts that broke for various reasons
|
commit | commitdiff | tree |
| 2010-10-17 |
Enrico Tassi | backport of patches to unification
|
commit | commitdiff | tree |
| 2010-10-17 |
Enrico Tassi | fixed List.for_all2 called without knowing if the two...
|
commit | commitdiff | tree |
| 2010-10-17 |
Enrico Tassi | new case for higher order unification:
|
commit | commitdiff | tree |
| 2010-10-17 |
Enrico Tassi | removed wrong optimization in delift and export is_flexible
|
commit | commitdiff | tree |
| 2010-10-01 |
Enrico Tassi | 16.2
|
commit | commitdiff | tree |
| 2010-09-30 |
Enrico Tassi | sync with stable:
|
commit | commitdiff | tree |
| 2010-09-30 |
Enrico Tassi | patches for hints & unification:
|
commit | commitdiff | tree |
| 2010-09-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-09-29 |
Enrico Tassi | hints for \epsilon
|
commit | commitdiff | tree |
| 2010-09-28 |
Enrico Tassi | hints polished and fixed to allow recursive inference...
|
commit | commitdiff | tree |
| 2010-09-28 |
Enrico Tassi | nicer hints, 16.1->3 done
|
commit | commitdiff | tree |
| 2010-09-27 |
Enrico Tassi | many fixes to setoids for re, 16.1 almost done
|
commit | commitdiff | tree |
| 2010-09-27 |
Enrico Tassi | fixed notation for \cup and \cap
|
commit | commitdiff | tree |
| 2010-09-25 |
Enrico Tassi | some reorganization + some more re-setoids.ma proofs
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | morphism support moved to sets/ and logic/cprop
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | interpretation for <->
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | fix typo
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | patch by Brian committed, cut&paste should not crash...
|
commit | commitdiff | tree |
| 2010-09-23 |
Enrico Tassi | Setoid-Rewriting under Ex works for an arbitrary depth...
|
commit | commitdiff | tree |
| 2010-09-16 |
Enrico Tassi | fixed notation
|
commit | commitdiff | tree |
| 2010-09-12 |
Enrico Tassi | some more work
|
commit | commitdiff | tree |
| 2010-09-12 |
Enrico Tassi | Change (or better define) the order of hints premises.
|
commit | commitdiff | tree |
| 2010-09-12 |
Enrico Tassi | non uniform coercions landed in hints_declaration.ma...
|
commit | commitdiff | tree |
| 2010-09-09 |
Enrico Tassi | Some refactoring in set*.ma, some new notations and...
|
commit | commitdiff | tree |
| 2010-09-09 |
Enrico Tassi | th 16.2 proved in the setoids setting
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | better not allowed sort elimination error messsage
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-09-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-29 |
Enrico Tassi | interpret non ambiguous symbols ASAP
|
commit | commitdiff | tree |
| 2010-07-28 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-28 |
Enrico Tassi | allows auto before eq is defined
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | some work on \exists
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | eq -> eq0 renaming
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | useless box removed
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | fixed precedence so that no () are needed around variable...
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | do not apply hints if metaclosed
|
commit | commitdiff | tree |
| 2010-07-22 |
Enrico Tassi | avoid assert false, just fail generating the coercion
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-21 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-20 |
Enrico Tassi | completed lemma 17
|
commit | commitdiff | tree |
| 2010-07-19 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-07-15 |
Enrico Tassi | re 16.4 almost done
|
commit | commitdiff | tree |
| 2010-07-10 |
Enrico Tassi | big mess of notation
|
commit | commitdiff | tree |
| 2010-07-09 |
Enrico Tassi | more notation
|
commit | commitdiff | tree |
| 2010-07-07 |
Enrico Tassi | moved formal_topology into library"
|
commit | commitdiff | tree |
| 2010-07-06 |
Enrico Tassi | some notation for map_arrows2
|
commit | commitdiff | tree |
| 2010-07-01 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-30 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2010-06-29 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-06-29 |
Enrico Tassi | notation made half decent
|
commit | commitdiff | tree |
| 2010-06-28 |
Enrico Tassi | better notation for oalgebra
|
commit | commitdiff | tree |
| 2010-06-18 |
Enrico Tassi | ....
|
commit | commitdiff | tree |
| 2010-06-17 |
Enrico Tassi | off by one fixed
|
commit | commitdiff | tree |
| 2010-06-07 |
Enrico Tassi | some stuff on re
|
commit | commitdiff | tree |
| 2010-06-07 |
Enrico Tassi | unify left args of inductive types with left argus...
|
commit | commitdiff | tree |
| 2010-05-11 |
Enrico Tassi | little workaround for multiple screens, gdk support...
|
commit | commitdiff | tree |
| 2010-05-10 |
Enrico Tassi | new intro:
|
commit | commitdiff | tree |
| 2010-05-07 |
Enrico Tassi | trace generation with "// by _;"
|
commit | commitdiff | tree |
| 2010-05-07 |
Enrico Tassi | notation
|
commit | commitdiff | tree |
| 2010-04-15 |
Enrico Tassi | bool_ext on 'o' not on 'Prop' (they are convertible...
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | fixed makefile
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | auto destructs while introducing in the context
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | print nobjects (hack with Obj.magic)
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | catch the right exception, avoid uncaught Subst_not_found
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | same heads different arity -> INCOMPARABLE
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | some fixes to THF parser
|
commit | commitdiff | tree |
| 2010-04-13 |
Enrico Tassi | fixed support file for TPTP
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | support axioms
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | ...
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | thf problems list for tptp 4.0.1
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | fixed compiltion order of lexer/parser
|
commit | commitdiff | tree |
| 2010-04-08 |
Enrico Tassi | THF parser received some care
|
commit | commitdiff | tree |
| 2010-04-07 |
Enrico Tassi | THF parser for TPTP
|
commit | commitdiff | tree |
| 2010-03-02 |
Enrico Tassi | Constants are indexed using the Reference, not the...
|
commit | commitdiff | tree |
| 2010-02-11 |
Enrico Tassi | minimal sequent height set to 1
|
commit | commitdiff | tree |
| next |
projects / helm.git / search