| 2008-05-17 |
Claudio Sacerdoti... | Missing check implemented: the sort of each constructors...
|
commit | commitdiff | tree |
| 2008-05-17 |
Claudio Sacerdoti... | The file bug_universi.ma shows a strage case where...
|
commit | commitdiff | tree |
| 2008-05-17 |
Claudio Sacerdoti... | Missing whd.
|
commit | commitdiff | tree |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed: since circular <= graphs are allowed, added...
|
commit | commitdiff | tree |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed: only Type < Type1 was declared.
|
commit | commitdiff | tree |
| 2008-05-17 |
Claudio Sacerdoti... | Bug fixed and further code semplification in management...
|
commit | commitdiff | tree |
| 2008-05-17 |
Claudio Sacerdoti... | The code for universes was not correct in many borderline...
|
commit | commitdiff | tree |
| 2008-05-15 |
Claudio Sacerdoti... | Timings
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | list_iter2_default_value moved to HExtlib. 1 euro to...
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | eat_lambdas and eat_or_subst_lambdas taken out of the...
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | debruijn simplified. It could go in nCicUtils, but...
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | Bug fixed: types were check for conversion in the wrong...
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | We forgot an important check: the declared and expected...
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | New checks for well-formedness of metasenvs and substs.
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | nuri_of_ouri, ouri_of_nuri, reference_of_ouri, ouri_of_refer...
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | Nicer graph.
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | map_hash moved to HExtlib
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | New function map_hash.
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | Generation of dot file.
|
commit | commitdiff | tree |
| 2008-05-14 |
Claudio Sacerdoti... | New licence used uniformly everywhere.
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | One more bug fixed: we tried to perform List.nth on...
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | More exceptions captured.
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | Bug fixed in pretty-printing of free Rels.
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | Never commit before trying to compile... stupid typo...
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | Used old kernel exception in place of brand new one.
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | - is_closed removed from the kernel (it used to make...
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | Library factorized out.
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | Type of conjecture and subst_entry made uniform.
|
commit | commitdiff | tree |
| 2008-05-13 |
Claudio Sacerdoti... | Added boolean "is_inductive" to NReference.Ind
|
commit | commitdiff | tree |
| 2008-05-12 |
Claudio Sacerdoti... | trust is always false by default
|
commit | commitdiff | tree |
| 2008-05-12 |
Claudio Sacerdoti... | trust implemented, but in the nCicTypeChecker!
|
commit | commitdiff | tree |
| 2008-05-12 |
Claudio Sacerdoti... | New implementation of CicEnvironment:
|
commit | commitdiff | tree |
| 2008-05-09 |
Claudio Sacerdoti... | Bug fixed: the domain of a LetRec was only made by...
|
commit | commitdiff | tree |
| 2008-05-07 |
Claudio Sacerdoti... | Update after some more bug fixing.
|
commit | commitdiff | tree |
| 2008-05-07 |
Claudio Sacerdoti... | Partially reverted bad merge by Enrico that re-introduced...
|
commit | commitdiff | tree |
| 2008-05-05 |
Claudio Sacerdoti... | More bugs fixed.
|
commit | commitdiff | tree |
| 2008-05-03 |
Claudio Sacerdoti... | Bug fixed in handling of explicit named substitutions...
|
commit | commitdiff | tree |
| 2008-05-03 |
Claudio Sacerdoti... | Broken XML files either fixed or removed.
|
commit | commitdiff | tree |
| 2008-05-01 |
Claudio Sacerdoti... | More precise classification of failures.
|
commit | commitdiff | tree |
| 2008-05-01 |
Claudio Sacerdoti... | List of all URIS comprising:
|
commit | commitdiff | tree |
| 2008-05-01 |
Claudio Sacerdoti... | More options can now be set at the beginning of the...
|
commit | commitdiff | tree |
| 2008-05-01 |
Claudio Sacerdoti... | Last (???) bug about variables with bodies fixed: we...
|
commit | commitdiff | tree |
| 2008-05-01 |
Claudio Sacerdoti... | Another case where the presence of variables with bodies...
|
commit | commitdiff | tree |
| 2008-05-01 |
Claudio Sacerdoti... | Bug fixed: application without arguments generated...
|
commit | commitdiff | tree |
| 2008-05-01 |
Claudio Sacerdoti... | New bug found.
|
commit | commitdiff | tree |
| 2008-04-30 |
Claudio Sacerdoti... | Things are getting better.
|
commit | commitdiff | tree |
| 2008-04-30 |
Claudio Sacerdoti... | Implementation of guarded_by_destructor is now complete...
|
commit | commitdiff | tree |
| 2008-04-30 |
Claudio Sacerdoti... | Reducing an open term should not be an error (or should...
|
commit | commitdiff | tree |
| 2008-04-30 |
Claudio Sacerdoti... | stupid error fixed
|
commit | commitdiff | tree |
| 2008-04-30 |
Claudio Sacerdoti... | fixed_args fixed to accept passing a partially applied...
|
commit | commitdiff | tree |
| 2008-04-29 |
Claudio Sacerdoti... | Tests status update.
|
commit | commitdiff | tree |
| 2008-04-28 |
Claudio Sacerdoti... | Avoid (whd ~delta:true) during guarded_by_destructors...
|
commit | commitdiff | tree |
| 2008-04-28 |
Claudio Sacerdoti... | In guarded by destructors, avoid computing the (whd...
|
commit | commitdiff | tree |
| 2008-04-24 |
Claudio Sacerdoti... | Update...
|
commit | commitdiff | tree |
| 2008-04-24 |
Claudio Sacerdoti... | No more bugs on guarded_by_constructors in the old...
|
commit | commitdiff | tree |
| 2008-04-24 |
Claudio Sacerdoti... | When going under a binder, a term must be converted...
|
commit | commitdiff | tree |
| 2008-04-24 |
Claudio Sacerdoti... | Working and broken URIs.
|
commit | commitdiff | tree |
| 2008-04-23 |
Claudio Sacerdoti... | Avoid other comparisons on universes using =.
|
commit | commitdiff | tree |
| 2008-04-23 |
Claudio Sacerdoti... | Avoid code duplication.
|
commit | commitdiff | tree |
| 2008-04-23 |
Claudio Sacerdoti... | Do NOT dare using Pervasives.compare on data structures...
|
commit | commitdiff | tree |
| 2008-04-22 |
Claudio Sacerdoti... | Types for LetIns computed during parsing for Coq objects...
|
commit | commitdiff | tree |
| 2008-04-21 |
Claudio Sacerdoti... | defn2.ma is to be used with part1a_inversion3
|
commit | commitdiff | tree |
| 2008-04-20 |
Claudio Sacerdoti... | Alternative prove using just one induction/inversion...
|
commit | commitdiff | tree |
| 2008-04-19 |
Claudio Sacerdoti... | oblivion_ugraph => empty_ugraph
|
commit | commitdiff | tree |
| 2008-04-19 |
Claudio Sacerdoti... | Added to flags to activate/disactivate pretty-printing...
|
commit | commitdiff | tree |
| 2008-04-19 |
Claudio Sacerdoti... | Uris must be stripped of their xpointers.
|
commit | commitdiff | tree |
| 2008-04-18 |
Claudio Sacerdoti... | Dead code removed.
|
commit | commitdiff | tree |
| 2008-04-18 |
Claudio Sacerdoti... | Inversion lemma for Forall.
|
commit | commitdiff | tree |
| 2008-04-15 |
Claudio Sacerdoti... | check_is_really_smaller simplified to consider that...
|
commit | commitdiff | tree |
| 2008-04-15 |
Claudio Sacerdoti... | 1. bug fixed: the context must be type-checked before...
|
commit | commitdiff | tree |
| 2008-04-15 |
Claudio Sacerdoti... | added sample of guarded by in which coq is stronger
|
commit | commitdiff | tree |
| 2008-04-11 |
Claudio Sacerdoti... | Extracted code. The main executable is medium_tests...
|
commit | commitdiff | tree |
| 2008-04-10 |
Claudio Sacerdoti... | The cache of objects is now used also for cofixpoints.
|
commit | commitdiff | tree |
| 2008-04-10 |
Claudio Sacerdoti... | New: cache of translated fixpoints (to avoid the generative...
|
commit | commitdiff | tree |
| 2008-04-10 |
Claudio Sacerdoti... | does_not_occur exported to be used in oCic2NCic
|
commit | commitdiff | tree |
| 2008-04-09 |
Claudio Sacerdoti... | Bug fixed: references to CoFix are CoFix, not Fix.
|
commit | commitdiff | tree |
| 2008-04-09 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-04-09 |
Claudio Sacerdoti... | Fixed serious bug that occurred only in the following...
|
commit | commitdiff | tree |
| 2008-04-09 |
Claudio Sacerdoti... | Added some "\n" here and there to the pretty-printing...
|
commit | commitdiff | tree |
| 2008-04-09 |
Claudio Sacerdoti... | Grave bug fixed: Ce that point to definitions were...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Variables are no longer experted (cooking is now implemented).
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Swapped arguments in error message.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Variables having a body can occur in cooked terms and...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Fix over the previous one: Var-LetIn abstractions should...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Error message improved.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Cooking w.r.t. variables with bodies is now implemented...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Fix name capture in cofix.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | To test the translation.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Name capture fixed.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Improved error messages in place of "sort elimination...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Seed reset before each convert_obj.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Use seed to avoid further name clashes.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Incredible, but true! Our name mangling clashed with...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Cooked objects are no longer well typed in the uncooked...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Improved eat_prods error message (at the cost of passing...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | The old kernel does not accept ens whose order is different...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Bad alpha-conversion by Enrico fixed.
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | Bug fixed: the ens need not be ordered w.r.t. the declared...
|
commit | commitdiff | tree |
| 2008-04-08 |
Claudio Sacerdoti... | j off by one in error message
|
commit | commitdiff | tree |
| next |
projects / helm.git / search