| 2009-05-14 |
Ferruccio Guidi | - hExtlib: added debugging information for split_nth |
blob | commitdiff | raw |
| 2009-02-02 |
Enrico Tassi | CicTypeChecker.typecheck now takes an additional parameter: |
blob | commitdiff | raw | diff to current |
| 2008-10-13 |
Claudio Sacerdoti... | Bug fixed in LetIn: the cumulativity test was performed... |
blob | commitdiff | raw | diff to current |
| 2008-09-07 |
Ferruccio Guidi | cicDischarge: we still have some problems here. Some... |
blob | commitdiff | raw | diff to current |
| 2008-08-01 |
Enrico Tassi | fixed recursiveness check |
blob | commitdiff | raw | diff to current |
| 2008-07-30 |
Enrico Tassi | fixed check, if 0 constructors then no List.nth is... |
blob | commitdiff | raw | diff to current |
| 2008-07-30 |
Enrico Tassi | allowed sort elim now check for recursive types |
blob | commitdiff | raw | diff to current |
| 2008-07-30 |
Claudio Sacerdoti... | Missing check implemented: uniformity of left parameter... |
blob | commitdiff | raw | diff to current |
| 2008-07-23 |
Enrico Tassi | positivity check fixed, some subterms were erroneously... |
blob | commitdiff | raw | diff to current |
| 2008-07-15 |
Enrico Tassi | CProp_i <= Type_i , Type_i <= CProp_i |
blob | commitdiff | raw | diff to current |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
blob | commitdiff | raw | diff to current |
| 2008-07-09 |
Enrico Tassi | tab -> ' ' |
blob | commitdiff | raw | diff to current |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
blob | commitdiff | raw | diff to current |
| 2008-05-29 |
Enrico Tassi | CProp, since it was defined in CoRN as a Type, is predi... |
blob | commitdiff | raw | diff to current |
| 2008-05-17 |
Enrico Tassi | impredicative Set is considered as Prop in the new... |
blob | commitdiff | raw | diff to current |
| 2008-05-17 |
Claudio Sacerdoti... | Missing check implemented: the sort of each constructor... |
blob | commitdiff | raw | diff to current |
| 2008-05-03 |
Claudio Sacerdoti... | Bug fixed in handling of explicit named substitutions... |
blob | commitdiff | raw | diff to current |
| 2008-04-28 |
Claudio Sacerdoti... | In guarded by destructors, avoid computing the (whd... |
blob | commitdiff | raw | diff to current |
| 2008-04-24 |
Enrico Tassi | guarded_by_constructor completely rewritten, fixed... |
blob | commitdiff | raw | diff to current |
| 2008-04-21 |
Enrico Tassi | fix universe handling, newly encountered objects are... |
blob | commitdiff | raw | diff to current |
| 2008-04-19 |
Enrico Tassi | ancient graph regarding universes and trust=false,... |
blob | commitdiff | raw | diff to current |
| 2008-04-19 |
Claudio Sacerdoti... | oblivion_ugraph => empty_ugraph |
blob | commitdiff | raw | diff to current |
| 2008-04-18 |
Enrico Tassi | cicEnvironment refactoring with sound view of Coq`s... |
blob | commitdiff | raw | diff to current |
| 2008-04-17 |
Enrico Tassi | example: |
blob | commitdiff | raw | diff to current |
| 2008-04-17 |
Enrico Tassi | added a missing whd |
blob | commitdiff | raw | diff to current |
| 2008-04-17 |
Enrico Tassi | new calculation of recursive parameters in guarded... |
blob | commitdiff | raw | diff to current |
| 2008-04-17 |
Enrico Tassi | Two similar cases packed together |
blob | commitdiff | raw | diff to current |
| 2008-04-17 |
Enrico Tassi | some fixes for guardness conditions |
blob | commitdiff | raw | diff to current |
| 2008-04-15 |
Claudio Sacerdoti... | check_is_really_smaller simplified to consider that... |
blob | commitdiff | raw | diff to current |
| 2008-04-15 |
Claudio Sacerdoti... | 1. bug fixed: the context must be type-checked before... |
blob | commitdiff | raw | diff to current |
| 2008-04-15 |
Enrico Tassi | positivity check fixed, a MutInd not applied (but with... |
blob | commitdiff | raw | diff to current |
| 2008-04-14 |
Enrico Tassi | positivity condition was relying on the name declared... |
blob | commitdiff | raw | diff to current |
| 2008-04-08 |
Claudio Sacerdoti... | Bad alpha-conversion by Enrico fixed. |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | the explicit type in a LetIn must be typecheckd before... |
blob | commitdiff | raw | diff to current |
| 2008-04-07 |
Enrico Tassi | lefts_and_tys was tys@lefts, CSC claims it was working... |
blob | commitdiff | raw | diff to current |
| 2008-04-03 |
Enrico Tassi | bug found rewriting the kernel backported: n instead... |
blob | commitdiff | raw | diff to current |
| 2008-04-02 |
Enrico Tassi | fixes backported from the new kernel |
blob | commitdiff | raw | diff to current |
| 2008-03-13 |
Claudio Sacerdoti... | :-( |
blob | commitdiff | raw | diff to current |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
blob | commitdiff | raw | diff to current |
| 2008-03-10 |
Claudio Sacerdoti... | Debugging print removed. |
blob | commitdiff | raw | diff to current |
| 2008-03-09 |
Claudio Sacerdoti... | Added ad-hoc optimization for check_metasenv_consistenc... |
blob | commitdiff | raw | diff to current |
| 2008-03-09 |
Claudio Sacerdoti... | Redundant check (because of an invariant) removed. |
blob | commitdiff | raw | diff to current |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: a MutCase with missing or exceeding cases... |
blob | commitdiff | raw | diff to current |
| 2007-03-22 |
Claudio Sacerdoti... | Several instances of the same bug fixed at once: when... |
blob | commitdiff | raw | diff to current |
| 2007-02-06 |
Claudio Sacerdoti... | Incredible bug fixed in Fix and CoFix. The types of... |
blob | commitdiff | raw | diff to current |
| 2006-10-23 |
Claudio Sacerdoti... | CicUniv.UniverseInconsistency is no handled correcly. |
blob | commitdiff | raw | diff to current |
| 2006-09-21 |
Enrico Tassi | "21" -> "Implicit found" |
blob | commitdiff | raw | diff to current |
| 2006-09-12 |
Claudio Sacerdoti... | Possible bug fixed (similar to the previous one, but... |
blob | commitdiff | raw | diff to current |
| 2006-09-12 |
Claudio Sacerdoti... | Bug fixed in the guarded_by_descructors function: in... |
blob | commitdiff | raw | diff to current |
| 2006-09-04 |
Andrea Asperti | Bug fixing. If the inductive types do not occur in... |
blob | commitdiff | raw | diff to current |
| 2006-03-29 |
Claudio Sacerdoti... | #### EXPERIMENTAL COMMIT #### |
blob | commitdiff | raw | diff to current |
| 2006-03-29 |
Claudio Sacerdoti... | Debugging code added. |
blob | commitdiff | raw | diff to current |
| 2006-03-28 |
Enrico Tassi | more profiling and fixes for paramod |
blob | commitdiff | raw | diff to current |
| 2006-03-27 |
Claudio Sacerdoti... | "Performance bug" fixed: I removed a whd in the does_no... |
blob | commitdiff | raw | diff to current |
| 2006-03-27 |
Claudio Sacerdoti... | Several "try ... with _ -> " specialized. |
blob | commitdiff | raw | diff to current |
| 2006-02-03 |
Stefano Zacchiroli | - renamed ocaml/ to components/ |
blob | commitdiff | raw | diff to current |
|
projects / helm.git / history