| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Bug fixed: when computing the left arguments, I was...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | New missing check implemented: the left parameters...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent types are no longer cleaned in inductive...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Dummy dependent products in inductive types arities...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | This commit avoids cleaning dummy dependent types in...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Implemented translation of inductive types from the...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Serious bug fixed: the max of two universes was computed...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Synch with the paper.
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | ...
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | Error message improved.
|
commit | commitdiff | tree |
| 2008-05-18 |
Claudio Sacerdoti... | More effective optimization: avoid introducing already...
|
commit | commitdiff | tree |
| 2008-05-17 |
Claudio Sacerdoti... | New check implemented: the sort of each constructor...
|
commit | commitdiff | tree |
| 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 |
| next |
projects / helm.git / search