| 2009-09-30 |
Claudio Sacerdoti... | With this hint, it diverges.
|
commit | commitdiff | tree |
| 2009-09-30 |
Claudio Sacerdoti... | New datatype for metasenv/subst: full fledged attributes...
|
commit | commitdiff | tree |
| 2009-09-30 |
Claudio Sacerdoti... | Better (but still broken) fix for the case ?sort vs...
|
commit | commitdiff | tree |
| 2009-09-30 |
Claudio Sacerdoti... | The term contains dummy.conv that was searched over...
|
commit | commitdiff | tree |
| 2009-09-29 |
Claudio Sacerdoti... | 1) improved (???) debugging, with
|
commit | commitdiff | tree |
| 2009-09-29 |
Claudio Sacerdoti... | Re-indentiation
|
commit | commitdiff | tree |
| 2009-09-29 |
Claudio Sacerdoti... | The unification does not longer use the refiner (urrah!)
|
commit | commitdiff | tree |
| 2009-09-29 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-09-29 |
Claudio Sacerdoti... | It does not work recursively...
|
commit | commitdiff | tree |
| 2009-09-29 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-09-28 |
Claudio Sacerdoti... | Experiment...
|
commit | commitdiff | tree |
| 2009-09-28 |
Claudio Sacerdoti... | Experiment...
|
commit | commitdiff | tree |
| 2009-09-18 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-09-16 |
Claudio Sacerdoti... | New interesting coercion.
|
commit | commitdiff | tree |
| 2009-09-16 |
Claudio Sacerdoti... | The left parameters coming from the constructor types...
|
commit | commitdiff | tree |
| 2009-09-14 |
Claudio Sacerdoti... | Slightly simplied status code.
|
commit | commitdiff | tree |
| 2009-09-14 |
Claudio Sacerdoti... | Simplest typing for status records.
|
commit | commitdiff | tree |
| 2009-09-14 |
Claudio Sacerdoti... | New tactics ncut and nlapply.
|
commit | commitdiff | tree |
| 2009-08-24 |
Claudio Sacerdoti... | Nicer proof "finished" (up to arithmetical facts).
|
commit | commitdiff | tree |
| 2009-08-21 |
Claudio Sacerdoti... | Towards a simplified proof.
|
commit | commitdiff | tree |
| 2009-08-21 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-20 |
Claudio Sacerdoti... | Injectivity proved! What a mess...
|
commit | commitdiff | tree |
| 2009-08-20 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-20 |
Claudio Sacerdoti... | - Bug fixed in definition of big_op.
|
commit | commitdiff | tree |
| 2009-08-20 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-19 |
Claudio Sacerdoti... | One half done.
|
commit | commitdiff | tree |
| 2009-08-19 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-18 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-18 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-18 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-14 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-14 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-14 |
Claudio Sacerdoti... | Since the introduction of saturation, an assert false...
|
commit | commitdiff | tree |
| 2009-08-13 |
Claudio Sacerdoti... | (nat,plus) is an abelian, unital magma
|
commit | commitdiff | tree |
| 2009-08-13 |
Claudio Sacerdoti... | Some quick patch to fix elimination that used to look for
|
commit | commitdiff | tree |
| 2009-08-13 |
Claudio Sacerdoti... | fix_sorts (cfr. previous commit) used to break too...
|
commit | commitdiff | tree |
| 2009-08-13 |
Claudio Sacerdoti... | Assert false do not allow to debug...
|
commit | commitdiff | tree |
| 2009-08-13 |
Claudio Sacerdoti... | Let's refresh the universe to avoid assert failure.
|
commit | commitdiff | tree |
| 2009-08-12 |
Claudio Sacerdoti... | A very little bit of arithmetic.
|
commit | commitdiff | tree |
| 2009-08-06 |
Claudio Sacerdoti... | The first omomorphism theorem for whole sets (i.e....
|
commit | commitdiff | tree |
| 2009-08-06 |
Claudio Sacerdoti... | Hmmm: I don't see much gain here.
|
commit | commitdiff | tree |
| 2009-08-06 |
Claudio Sacerdoti... | Metas must be handled when using iterators.
|
commit | commitdiff | tree |
| 2009-08-06 |
Claudio Sacerdoti... | Setoid rewriting as unification hinting. Does not work...
|
commit | commitdiff | tree |
| 2009-08-04 |
Claudio Sacerdoti... | More Gonthierism. Are they the right solution?
|
commit | commitdiff | tree |
| 2009-08-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-08-04 |
Claudio Sacerdoti... | Hmmm, quite broken now.
|
commit | commitdiff | tree |
| 2009-08-01 |
Claudio Sacerdoti... | Smaller formulae.
|
commit | commitdiff | tree |
| 2009-07-31 |
Claudio Sacerdoti... | Setoids, setoids1, sets, and the like. The mess begins.
|
commit | commitdiff | tree |
| 2009-07-31 |
Claudio Sacerdoti... | Bad patch reverted (in error message).
|
commit | commitdiff | tree |
| 2009-07-31 |
Claudio Sacerdoti... | Bug fixed: one case of too many arguments was not detected...
|
commit | commitdiff | tree |
| 2009-07-31 |
Claudio Sacerdoti... | Serious bug fixed: uris were not refreshed when loading...
|
commit | commitdiff | tree |
| 2009-07-31 |
Claudio Sacerdoti... | Record projections are now defined as fixpoints in...
|
commit | commitdiff | tree |
| 2009-07-31 |
Claudio Sacerdoti... | \ldots are now used in nelim and ncases
|
commit | commitdiff | tree |
| 2009-07-31 |
Claudio Sacerdoti... | Pp fixed in order to obtain read-back.
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | 1) \ldots here and there
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | More napply \ldots => napply
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | napply now automatically inserts \ldots at the end
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | More \ldots.
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | \ldots used here and there. Cool!
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | First implementation of \ldots.
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-30 |
Claudio Sacerdoti... | Don't reinvent the wheel.
|
commit | commitdiff | tree |
| 2009-07-28 |
Claudio Sacerdoti... | "..." -> "\ldots" for implicit vectors
|
commit | commitdiff | tree |
| 2009-07-28 |
Claudio Sacerdoti... | 1) Some more work for vector implicits.
|
commit | commitdiff | tree |
| 2009-07-28 |
Claudio Sacerdoti... | Introduction of vectors of implicit (only for NG).
|
commit | commitdiff | tree |
| 2009-07-27 |
Claudio Sacerdoti... | Stupid bug fixed: the test to detect Uncertain cases...
|
commit | commitdiff | tree |
| 2009-07-27 |
Claudio Sacerdoti... | Useless "let module" removed.
|
commit | commitdiff | tree |
| 2009-07-27 |
Claudio Sacerdoti... | Since I guess the divergence bug is fixed, I activate...
|
commit | commitdiff | tree |
| 2009-07-27 |
Claudio Sacerdoti... | Serious bug fixed: because of lazy evaluation of !require1...
|
commit | commitdiff | tree |
| 2009-07-27 |
Claudio Sacerdoti... | setoids.ma split into setoids.ma + setoids1.ma
|
commit | commitdiff | tree |
| 2009-07-27 |
Claudio Sacerdoti... | topology/igt.ma (???) |-> sets/setoids.ma
|
commit | commitdiff | tree |
| 2009-07-27 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | It works better now.
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | No more hand-made coercions.
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | Debugging code removed.
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | Record fields declared as coercions as now really declared...
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | Beta-expansion was avoided as soon as one argument...
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | Function to map NCic.term to CicNotationPt.term finished.
|
commit | commitdiff | tree |
| 2009-07-24 |
Claudio Sacerdoti... | Bug (found during code review) fixed (but not tested...
|
commit | commitdiff | tree |
| 2009-07-23 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | Elimination principles are now processed in O(1) again
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | Major speed-up: meta-chains are now expanded during...
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | 1) PTS simplified
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | nelim fixed
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | leftno was List.length rights :-)
|
commit | commitdiff | tree |
| 2009-07-22 |
Claudio Sacerdoti... | Almost ready to implement coercion declaration for...
|
commit | commitdiff | tree |
| 2009-07-21 |
Claudio Sacerdoti... | 1) record projections are now automatically generated
|
commit | commitdiff | tree |
| 2009-07-21 |
Claudio Sacerdoti... | Debugging code removed.
|
commit | commitdiff | tree |
| 2009-07-21 |
Claudio Sacerdoti... | Record projections are now automatically generated...
|
commit | commitdiff | tree |
| 2009-07-20 |
Claudio Sacerdoti... | Debugging printf removed
|
commit | commitdiff | tree |
| 2009-07-20 |
Claudio Sacerdoti... | nrewrite now uses the appropriate principle when going...
|
commit | commitdiff | tree |
| 2009-07-20 |
Claudio Sacerdoti... | nrewrite now working
|
commit | commitdiff | tree |
| 2009-07-20 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-07-20 |
Claudio Sacerdoti... | Very serious bug fixed in unification, but the fix...
|
commit | commitdiff | tree |
| 2009-07-20 |
Claudio Sacerdoti... | 1) The NG kernel now accepts only usage of declared...
|
commit | commitdiff | tree |
| 2009-07-20 |
Claudio Sacerdoti... | 1) ppmetasenv and ppcontext to reduce the amount of...
|
commit | commitdiff | tree |
| next |
projects / helm.git / search