| 2009-04-16 |
Claudio Sacerdoti... | Bug: let-ins are always automatically folded!
|
commit | commitdiff | tree |
| 2009-04-16 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-04-16 |
Claudio Sacerdoti... | test/a.ma => tests/ng_tactics.ma, with nassert here...
|
commit | commitdiff | tree |
| 2009-04-16 |
Claudio Sacerdoti... | Replaced long, bugged implementation of letin-tac with...
|
commit | commitdiff | tree |
| 2009-04-16 |
Claudio Sacerdoti... | Added ppterm.
|
commit | commitdiff | tree |
| 2009-04-16 |
Claudio Sacerdoti... | The context is now parsed in the reverse (right) order.
|
commit | commitdiff | tree |
| 2009-04-16 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-04-14 |
Claudio Sacerdoti... | Trick: the refiner always subst-expands the outtype...
|
commit | commitdiff | tree |
| 2009-04-14 |
Claudio Sacerdoti... | Bug fixed in two lines + 5 lines of comment.
|
commit | commitdiff | tree |
| 2009-04-14 |
Claudio Sacerdoti... | assert_tac now takes a list of sequents and also checks...
|
commit | commitdiff | tree |
| 2009-04-14 |
Claudio Sacerdoti... | New debugging tactic nassert:
|
commit | commitdiff | tree |
| 2009-04-12 |
Claudio Sacerdoti... | Semantic selection back again (but no semantic cut...
|
commit | commitdiff | tree |
| 2009-04-12 |
Claudio Sacerdoti... | Match is now rendered as best as possible.
|
commit | commitdiff | tree |
| 2009-04-10 |
Claudio Sacerdoti... | The sequent viewer now considers the context to render...
|
commit | commitdiff | tree |
| 2009-04-09 |
Claudio Sacerdoti... | The substitution is now taken in account when printing...
|
commit | commitdiff | tree |
| 2009-04-09 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-04-09 |
Claudio Sacerdoti... | + Chain NCic.term -> content -> presentation very...
|
commit | commitdiff | tree |
| 2009-04-08 |
Claudio Sacerdoti... | Just to make it compile again.
|
commit | commitdiff | tree |
| 2009-04-07 |
Claudio Sacerdoti... | - nrewrite ((very?) rough implementation)
|
commit | commitdiff | tree |
| 2009-04-07 |
Claudio Sacerdoti... | - more progress towards generalize, but I am stuck now
|
commit | commitdiff | tree |
| 2009-04-06 |
Claudio Sacerdoti... | New tactic clear; new syntax # _; to introduce and...
|
commit | commitdiff | tree |
| 2009-04-06 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic "case1_tac" that make "intro" followed by...
|
commit | commitdiff | tree |
| 2009-04-01 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-04-01 |
Claudio Sacerdoti... | ## prefix is now used for tinycals
|
commit | commitdiff | tree |
| 2009-04-01 |
Claudio Sacerdoti... | New tactic intro. Syntax: "# n".
|
commit | commitdiff | tree |
| 2009-03-19 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-03-12 |
Claudio Sacerdoti... | More details on the proof.
|
commit | commitdiff | tree |
| 2009-03-12 |
Claudio Sacerdoti... | New algorithm based on in-place modification of the...
|
commit | commitdiff | tree |
| 2009-03-06 |
Claudio Sacerdoti... | Minor improvements in pretty-printing.
|
commit | commitdiff | tree |
| 2009-03-05 |
Claudio Sacerdoti... | New version: only new nodes are normalized; moreover...
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | New version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | First version.
|
commit | commitdiff | tree |
| 2009-03-02 |
Claudio Sacerdoti... | Old algorithm moved to old to leave place to the new...
|
commit | commitdiff | tree |
| 2009-02-02 |
Claudio Sacerdoti... | Hmmm, going too low.
|
commit | commitdiff | tree |
| 2009-02-02 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-02-01 |
Claudio Sacerdoti... | Towards fullness.
|
commit | commitdiff | tree |
| 2009-02-01 |
Claudio Sacerdoti... | Renaming.
|
commit | commitdiff | tree |
| 2009-02-01 |
Claudio Sacerdoti... | Renaming.
|
commit | commitdiff | tree |
| 2009-01-22 |
Claudio Sacerdoti... | TODO
|
commit | commitdiff | tree |
| 2009-01-19 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-01-19 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-01-18 |
Claudio Sacerdoti... | universe inconsistency fixed
|
commit | commitdiff | tree |
| 2009-01-18 |
Claudio Sacerdoti... | SUBSETS_full up to universe inconsistency
|
commit | commitdiff | tree |
| 2009-01-17 |
Claudio Sacerdoti... | faithful
|
commit | commitdiff | tree |
| 2009-01-17 |
Claudio Sacerdoti... | CAT2
|
commit | commitdiff | tree |
| 2009-01-16 |
Claudio Sacerdoti... | Sambin's result holds trivially since most of the fields...
|
commit | commitdiff | tree |
| 2009-01-16 |
Claudio Sacerdoti... | basic topologies are trivially o-basic topologies
|
commit | commitdiff | tree |
| 2009-01-16 |
Claudio Sacerdoti... | 1. new coercion(s) from CPropi to CProp
|
commit | commitdiff | tree |
| 2009-01-14 |
Claudio Sacerdoti... | o_continous_relations are really o_relation_pair.....
|
commit | commitdiff | tree |
| 2009-01-14 |
Claudio Sacerdoti... | o-basic_pairs are indeed examples of o-basic_topologies!
|
commit | commitdiff | tree |
| 2009-01-13 |
Claudio Sacerdoti... | - Added new output in standard C.
|
commit | commitdiff | tree |
| 2009-01-12 |
Claudio Sacerdoti... | Some work on o-algebras towards the proof that a and...
|
commit | commitdiff | tree |
| 2009-01-08 |
Claudio Sacerdoti... | The new coercion from SET to Type0 with higher priority...
|
commit | commitdiff | tree |
| 2009-01-08 |
Claudio Sacerdoti... | Just a snapshot.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | More work on concrete spaces.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Some work on concrete spaces.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Cool: only 8 universes in use.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | 1) Some reorganization.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Some renaming to avoid confusion between saturations...
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Fixing universe levels for saturations and (partially...
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | The functor from BP to OBP has been defined (but no...
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Ok, even if not stated formally, now we know that the...
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | orelation_of_relation preserves equality and identities.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Basic pairs restored; require renaming to use them...
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Some progress: everything works well now.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Ooops, I forgot to commit this in the previous 3-4...
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | An hint moved to the right place.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | No more daemons, no more exTs.
|
commit | commitdiff | tree |
| 2009-01-06 |
Claudio Sacerdoti... | Great: some significant progress in fixing universe...
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | 1. CProp_n fixed to be equal to Type_n to better understand...
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | Snapshot to try to understand something.
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | Some more progress, fighting universe inconsistencies.
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | Yet another universe problem :-(
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | Back to step 1: all files that used to pass now pass...
|
commit | commitdiff | tree |
| 2009-01-04 |
Claudio Sacerdoti... | More re-organization.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Basic pairs went through with no problems.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Universe level fixed (litterally).
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Niceness was just a temporary illusion :-(
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Much, much nicer now.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | Some more re-organization.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | More re-working.
|
commit | commitdiff | tree |
| 2009-01-03 |
Claudio Sacerdoti... | More reorganization.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | equivalence_relations made uniform w.r.t. universe...
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Final work for today.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Some more painful work.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | binary_meet is back again, with some effort
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Many universe inconsistency avoided here and there.
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | The universe inconsistency comes from big union, that...
|
commit | commitdiff | tree |
| 2008-12-28 |
Claudio Sacerdoti... | Proof that \Omega \sup A is an overlap algebra, up...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search