| 2008-05-07 |
Claudio Sacerdoti... | Update after some more bug fixing. |
commit | commitdiff | tree | snapshot |
| 2008-05-07 |
Claudio Sacerdoti... | Partially reverted bad merge by Enrico that re-introduc... |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Claudio Sacerdoti... | More bugs fixed. |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | get_check_fix and cofix unified, bug regarding debruijn... |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | get_checked_indtys can take a constructor reference |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | added mk_cofix |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | let corec |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | CoFix cache implemented |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | fix_left_in_constr still broken, ask enrico |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | guarded_by_constructors implemented, some cleanup here... |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | removed dead code |
commit | commitdiff | tree | snapshot |
| 2008-05-05 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-05-03 |
Claudio Sacerdoti... | Bug fixed in handling of explicit named substitutions... |
commit | commitdiff | tree | snapshot |
| 2008-05-03 |
Claudio Sacerdoti... | Broken XML files either fixed or removed. |
commit | commitdiff | tree | snapshot |
| 2008-05-02 |
Wilmer Ricciotti | Some destruct tactics got broken after last update... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | More precise classification of failures. |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | List of all URIS comprising: |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | More options can now be set at the beginning of the... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | Last (???) bug about variables with bodies fixed: we... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | Another case where the presence of variables with bodie... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Enrico Tassi | tagging 0.5.0-rc1 |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | Bug fixed: application without arguments generated... |
commit | commitdiff | tree | snapshot |
| 2008-05-01 |
Claudio Sacerdoti... | New bug found. |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Claudio Sacerdoti... | Things are getting better. |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Claudio Sacerdoti... | Implementation of guarded_by_destructor is now complete... |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Claudio Sacerdoti... | Reducing an open term should not be an error (or should... |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Claudio Sacerdoti... | stupid error fixed |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Claudio Sacerdoti... | fixed_args fixed to accept passing a partially applied... |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | added check on all bodies, only the one we actually... |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | added fake uri when the univ is anon |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | fixed wrong Rel, still to do: Fix(i,j) applied to dange... |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | universes are written with the URI inside objects,... |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | xml strict! |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | many pending modifications were there, now the website... |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | guarded_by_destructors on steroids |
commit | commitdiff | tree | snapshot |
| 2008-04-30 |
Enrico Tassi | added list_mapi |
commit | commitdiff | tree | snapshot |
| 2008-04-29 |
Claudio Sacerdoti... | Tests status update. |
commit | commitdiff | tree | snapshot |
| 2008-04-29 |
Enrico Tassi | speedup in fixing the graph closures |
commit | commitdiff | tree | snapshot |
| 2008-04-28 |
Claudio Sacerdoti... | Avoid (whd ~delta:true) during guarded_by_destructors... |
commit | commitdiff | tree | snapshot |
| 2008-04-28 |
Claudio Sacerdoti... | In guarded by destructors, avoid computing the (whd... |
commit | commitdiff | tree | snapshot |
| 2008-04-24 |
Claudio Sacerdoti... | Update... |
commit | commitdiff | tree | snapshot |
| 2008-04-24 |
Claudio Sacerdoti... | No more bugs on guarded_by_constructors in the old... |
commit | commitdiff | tree | snapshot |
| 2008-04-24 |
Claudio Sacerdoti... | When going under a binder, a term must be converted... |
commit | commitdiff | tree | snapshot |
| 2008-04-24 |
Wilmer Ricciotti | Proof of adequacy. |
commit | commitdiff | tree | snapshot |
| 2008-04-24 |
Enrico Tassi | guarded_by_constructor completely rewritten, fixed... |
commit | commitdiff | tree | snapshot |
| 2008-04-24 |
Enrico Tassi | added coinductive example |
commit | commitdiff | tree | snapshot |
| 2008-04-24 |
Claudio Sacerdoti... | Working and broken URIs. |
commit | commitdiff | tree | snapshot |
| 2008-04-23 |
Enrico Tassi | ported the instantiate-left-params-to-calculate-rec... |
commit | commitdiff | tree | snapshot |
| 2008-04-23 |
Claudio Sacerdoti... | Avoid other comparisons on universes using =. |
commit | commitdiff | tree | snapshot |
| 2008-04-23 |
Claudio Sacerdoti... | Avoid code duplication. |
commit | commitdiff | tree | snapshot |
| 2008-04-23 |
Claudio Sacerdoti... | Do NOT dare using Pervasives.compare on data structures... |
commit | commitdiff | tree | snapshot |
| 2008-04-22 |
Enrico Tassi | oblivion ugraph everywhere outside the kernel |
commit | commitdiff | tree | snapshot |
| 2008-04-22 |
Enrico Tassi | slow_implementation and some dead code removed |
commit | commitdiff | tree | snapshot |
| 2008-04-22 |
Enrico Tassi | more strict check by CSC, I miss it |
commit | commitdiff | tree | snapshot |
| 2008-04-22 |
Enrico Tassi | fix cache comparison relaxed to URI and not REFERENCE |
commit | commitdiff | tree | snapshot |
| 2008-04-22 |
Enrico Tassi | added a call to ppcontext in the case of appl, to ease... |
commit | commitdiff | tree | snapshot |
| 2008-04-22 |
Enrico Tassi | added ppcontext |
commit | commitdiff | tree | snapshot |
| 2008-04-22 |
Claudio Sacerdoti... | Types for LetIns computed during parsing for Coq object... |
commit | commitdiff | tree | snapshot |
| 2008-04-21 |
Claudio Sacerdoti... | defn2.ma is to be used with part1a_inversion3 |
commit | commitdiff | tree | snapshot |
| 2008-04-21 |
Enrico Tassi | fix universe handling, newly encountered objects are... |
commit | commitdiff | tree | snapshot |
| 2008-04-20 |
Claudio Sacerdoti... | Alternative prove using just one induction/inversion... |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | better error message |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | ... |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | impredicative set work around |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | impredicative set work around |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | associativity of -> fixed |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | ancient graph regarding universes and trust=false,... |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | extlib list_uniq instead of local copy |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | ranking function fixed: when graphs are collapsed one... |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Enrico Tassi | added flag to change Set into Type on the fly, that... |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Claudio Sacerdoti... | oblivion_ugraph => empty_ugraph |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Claudio Sacerdoti... | Added to flags to activate/disactivate pretty-printing... |
commit | commitdiff | tree | snapshot |
| 2008-04-19 |
Claudio Sacerdoti... | Uris must be stripped of their xpointers. |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Claudio Sacerdoti... | Dead code removed. |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Claudio Sacerdoti... | Inversion lemma for Forall. |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Enrico Tassi | workaround for Pi associativity |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Enrico Tassi | workaround for some Set/Type problems |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Enrico Tassi | cicEnvironment refactoring with sound view of Coq`s... |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Enrico Tassi | assertion was wrong, an object can contain a named... |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Enrico Tassi | graph generation phase fixed |
commit | commitdiff | tree | snapshot |
| 2008-04-18 |
Enrico Tassi | Appl case in is_really_smaller fixed as in the old... |
commit | commitdiff | tree | snapshot |
| 2008-04-17 |
Enrico Tassi | example: |
commit | commitdiff | tree | snapshot |
| 2008-04-17 |
Enrico Tassi | added a missing whd |
commit | commitdiff | tree | snapshot |
| 2008-04-17 |
Enrico Tassi | new calculation of recursive parameters in guarded... |
commit | commitdiff | tree | snapshot |
| 2008-04-17 |
Enrico Tassi | Two similar cases packed together |
commit | commitdiff | tree | snapshot |
| 2008-04-17 |
Enrico Tassi | some fixes for guardness conditions |
commit | commitdiff | tree | snapshot |
| 2008-04-17 |
Enrico Tassi | is_really_smaller in sync with old kernel, impossible... |
commit | commitdiff | tree | snapshot |
| 2008-04-15 |
Claudio Sacerdoti... | check_is_really_smaller simplified to consider that... |
commit | commitdiff | tree | snapshot |
| 2008-04-15 |
Claudio Sacerdoti... | 1. bug fixed: the context must be type-checked before... |
commit | commitdiff | tree | snapshot |
| 2008-04-15 |
Enrico Tassi | get_checked_fix -> get_checked_fixes |
commit | commitdiff | tree | snapshot |
| 2008-04-15 |
Enrico Tassi | added comment |
commit | commitdiff | tree | snapshot |
| 2008-04-15 |
Claudio Sacerdoti... | added sample of guarded by in which coq is stronger |
commit | commitdiff | tree | snapshot |
| 2008-04-15 |
Enrico Tassi | positivity check fixed, a MutInd not applied (but with... |
commit | commitdiff | tree | snapshot |
| 2008-04-15 |
Enrico Tassi | do not use an implicit but a sort as a neutral term... |
commit | commitdiff | tree | snapshot |
| 2008-04-14 |
Enrico Tassi | objects are typechecked to ensure there is a graph... |
commit | commitdiff | tree | snapshot |
| 2008-04-14 |
Enrico Tassi | leftno should be increased of the expnamedsubst, but... |
commit | commitdiff | tree | snapshot |
| 2008-04-14 |
Enrico Tassi | better error message |
commit | commitdiff | tree | snapshot |
| 2008-04-14 |
Enrico Tassi | same_obj made more precise, fixed the order of the... |
commit | commitdiff | tree | snapshot |
| 2008-04-14 |
Enrico Tassi | ficed fixpoint cache usage for mutual fix |
commit | commitdiff | tree | snapshot |
| 2008-04-14 |
Enrico Tassi | fixed positivity conditions |
commit | commitdiff | tree | snapshot |
| next |
projects / helm.git / shortlog