| 2009-11-04 |
Claudio Sacerdoti... | 1) sort computation undone (it used to be bugged anyway)
|
commit | commitdiff | tree |
| 2009-10-30 |
Claudio Sacerdoti... | Code simplified.
|
commit | commitdiff | tree |
| 2009-10-30 |
Claudio Sacerdoti... | Useless old code for ad-hoc management of out-scope...
|
commit | commitdiff | tree |
| 2009-10-30 |
Claudio Sacerdoti... | New style debugging/profiling for NCicMetaSubst.
|
commit | commitdiff | tree |
| 2009-10-30 |
Claudio Sacerdoti... | Sometimes it is useful to be able to print the subst...
|
commit | commitdiff | tree |
| 2009-10-29 |
Claudio Sacerdoti... | Better error message.
|
commit | commitdiff | tree |
| 2009-10-29 |
Claudio Sacerdoti... | For some obscure reason, more universes are now needed...
|
commit | commitdiff | tree |
| 2009-10-29 |
Claudio Sacerdoti... | instantiate/sortfy/kindfy etc. reimplemented with less...
|
commit | commitdiff | tree |
| 2009-10-29 |
Claudio Sacerdoti... | New function.
|
commit | commitdiff | tree |
| 2009-10-29 |
Claudio Sacerdoti... | Let's use already existent functions.
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | Works again
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | Ad-hoc management of ? vs out_scope in instantiate...
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | Bug fixed: the `IsTerm attribute is now added by mk_meta...
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | 1) new-style debugging/profiling code for old reduction
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | Commented out code to optimize the case t1 vs t2 when...
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | One-shot aliases were no longer generated because of...
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | Different aliases, better equality inferred.
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | instances
|
commit | commitdiff | tree |
| 2009-10-28 |
Claudio Sacerdoti... | instance fixed
|
commit | commitdiff | tree |
| 2009-10-26 |
Claudio Sacerdoti... | qed => nqed.
|
commit | commitdiff | tree |
| 2009-10-26 |
Claudio Sacerdoti... | Now the time required to eval a command is printed.
|
commit | commitdiff | tree |
| 2009-10-23 |
Claudio Sacerdoti... | Alias required now ??
|
commit | commitdiff | tree |
| 2009-10-21 |
Claudio Sacerdoti... | Non general recursion implemented via recursion over...
|
commit | commitdiff | tree |
| 2009-10-20 |
Claudio Sacerdoti... | - Bug fixed: some assert failure were just failures...
|
commit | commitdiff | tree |
| 2009-10-19 |
Claudio Sacerdoti... | Smarter implementation of instantiate to avoid re-checking...
|
commit | commitdiff | tree |
| 2009-10-15 |
Claudio Sacerdoti... | Profiling code integrated.
|
commit | commitdiff | tree |
| 2009-10-14 |
Claudio Sacerdoti... | Debugging improved.
|
commit | commitdiff | tree |
| 2009-10-14 |
Claudio Sacerdoti... | Benchmarking integrated in folding/unfolding.
|
commit | commitdiff | tree |
| 2009-10-14 |
Claudio Sacerdoti... | Error message fixed (dereferencing must be done eagerly...
|
commit | commitdiff | tree |
| 2009-10-14 |
Claudio Sacerdoti... | Serious bug fixed: fix_sorts used to allow inference...
|
commit | commitdiff | tree |
| 2009-10-12 |
Claudio Sacerdoti... | 1) Bug fixed: the case Meta(i) vs Meta(i) was handled...
|
commit | commitdiff | tree |
| 2009-10-12 |
Claudio Sacerdoti... | Bug fixed: in case of (t ...) where t has flexible...
|
commit | commitdiff | tree |
| 2009-10-12 |
Claudio Sacerdoti... | Typo fixed.
|
commit | commitdiff | tree |
| 2009-10-12 |
Claudio Sacerdoti... | Closed metas must have closed (expected) types.
|
commit | commitdiff | tree |
| 2009-10-12 |
Claudio Sacerdoti... | Improved debugging code.
|
commit | commitdiff | tree |
| 2009-10-08 |
Claudio Sacerdoti... | A new switch to activate/deactive nCicReduction pretty...
|
commit | commitdiff | tree |
| 2009-10-08 |
Claudio Sacerdoti... | Printing extremely large terms no longer raises Failure.
|
commit | commitdiff | tree |
| 2009-10-07 |
Claudio Sacerdoti... | Performance improvement by preserving more sharing...
|
commit | commitdiff | tree |
| 2009-10-07 |
Claudio Sacerdoti... | Debugging code commented out.
|
commit | commitdiff | tree |
| 2009-10-07 |
Claudio Sacerdoti... | - oCic2NCic and nCic2OCic moved to ng_library
|
commit | commitdiff | tree |
| 2009-10-06 |
Claudio Sacerdoti... | Improved error message.
|
commit | commitdiff | tree |
| 2009-10-05 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-05 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-05 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-04 |
Claudio Sacerdoti... | Does not compile! Wrong unification hint?
|
commit | commitdiff | tree |
| 2009-10-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-04 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2009-10-02 |
Claudio Sacerdoti... | Wrong context (again!)
|
commit | commitdiff | tree |
| 2009-10-02 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / helm.git / search