| 2008-07-15 |
Enrico Tassi | CProp_i <= Type_i , Type_i <= CProp_i |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | CProp hierarchy fixed: |
tree | commitdiff |
| 2008-07-09 |
Enrico Tassi | tab -> ' ' |
tree | commitdiff |
| 2008-05-30 |
Enrico Tassi | CProp hierarchy is there! |
tree | commitdiff |
| 2008-05-29 |
Enrico Tassi | CProp, since it was defined in CoRN as a Type, is predi... |
tree | commitdiff |
| 2008-05-17 |
Enrico Tassi | impredicative Set is considered as Prop in the new... |
tree | commitdiff |
| 2008-05-17 |
Claudio Sacerdoti... | Missing check implemented: the sort of each constructor... |
tree | commitdiff |
| 2008-05-03 |
Claudio Sacerdoti... | Bug fixed in handling of explicit named substitutions... |
tree | commitdiff |
| 2008-04-30 |
Enrico Tassi | universes are written with the URI inside objects,... |
tree | commitdiff |
| 2008-04-28 |
Claudio Sacerdoti... | In guarded by destructors, avoid computing the (whd... |
tree | commitdiff |
| 2008-04-24 |
Enrico Tassi | guarded_by_constructor completely rewritten, fixed... |
tree | commitdiff |
| 2008-04-21 |
Enrico Tassi | fix universe handling, newly encountered objects are... |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | ancient graph regarding universes and trust=false,... |
tree | commitdiff |
| 2008-04-19 |
Enrico Tassi | extlib list_uniq instead of local copy |
tree | commitdiff |
| 2008-04-19 |
Claudio Sacerdoti... | oblivion_ugraph => empty_ugraph |
tree | commitdiff |
| 2008-04-18 |
Enrico Tassi | cicEnvironment refactoring with sound view of Coq`s... |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | example: |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | added a missing whd |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | new calculation of recursive parameters in guarded... |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | Two similar cases packed together |
tree | commitdiff |
| 2008-04-17 |
Enrico Tassi | some fixes for guardness conditions |
tree | commitdiff |
| 2008-04-15 |
Claudio Sacerdoti... | check_is_really_smaller simplified to consider that... |
tree | commitdiff |
| 2008-04-15 |
Claudio Sacerdoti... | 1. bug fixed: the context must be type-checked before... |
tree | commitdiff |
| 2008-04-15 |
Enrico Tassi | positivity check fixed, a MutInd not applied (but with... |
tree | commitdiff |
| 2008-04-14 |
Enrico Tassi | positivity condition was relying on the name declared... |
tree | commitdiff |
| 2008-04-11 |
Enrico Tassi | Conversion of 2 lambdas was not requiring equality... |
tree | commitdiff |
| 2008-04-10 |
Claudio Sacerdoti... | does_not_occur exported to be used in oCic2NCic |
tree | commitdiff |
| 2008-04-09 |
Enrico Tassi | invalidate fixed |
tree | commitdiff |
| 2008-04-08 |
Claudio Sacerdoti... | Bad alpha-conversion by Enrico fixed. |
tree | commitdiff |
| 2008-04-07 |
Enrico Tassi | added invalidate to clear the cache and ease the compar... |
tree | commitdiff |
| 2008-04-07 |
Enrico Tassi | the explicit type in a LetIn must be typecheckd before... |
tree | commitdiff |
| 2008-04-07 |
Enrico Tassi | lefts_and_tys was tys@lefts, CSC claims it was working... |
tree | commitdiff |
| 2008-04-03 |
Enrico Tassi | bug found rewriting the kernel backported: n instead... |
tree | commitdiff |
| 2008-04-02 |
Enrico Tassi | fixes backported from the new kernel |
tree | commitdiff |
| 2008-03-13 |
Claudio Sacerdoti... | :-( |
tree | commitdiff |
| 2008-03-11 |
Claudio Sacerdoti... | Very experimental commit: the type of the source is... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | whd: ~delta=false now controls also zeta-reduction... |
tree | commitdiff |
| 2008-03-10 |
Claudio Sacerdoti... | Debugging print removed. |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Added ad-hoc optimization for check_metasenv_consistenc... |
tree | commitdiff |
| 2008-03-09 |
Claudio Sacerdoti... | Redundant check (because of an invariant) removed. |
tree | commitdiff |
| 2007-10-25 |
Claudio Sacerdoti... | Bug fixed: a MutCase with missing or exceeding cases... |
tree | commitdiff |
| 2007-10-12 |
Claudio Sacerdoti... | Move to OCaml 3.10. Requires debian packages from unsta... |
tree | commitdiff |
| 2007-07-19 |
Claudio Sacerdoti... | Convertibility now converts machines in place of terms. |
tree | commitdiff |
| 2007-07-10 |
Claudio Sacerdoti... | New reduction strategy: the new reduction strategy... |
tree | commitdiff |
| 2007-07-06 |
Enrico Tassi | maxipatch for support of multiple DBs. |
tree | commitdiff |
| 2007-05-29 |
Enrico Tassi | added some lines to compile for debugging |
tree | commitdiff |
| 2007-03-26 |
Claudio Sacerdoti... | Serious bug fixed: a variable was captured during unfol... |
tree | commitdiff |
| 2007-03-22 |
Claudio Sacerdoti... | Several instances of the same bug fixed at once: when... |
tree | commitdiff |
| 2007-03-22 |
Claudio Sacerdoti... | Debugging code removed. |
tree | commitdiff |
| 2007-03-16 |
Ferruccio Guidi | elim tactic: it needs two arguments, a term as well... |
tree | commitdiff |
| 2007-03-13 |
Andrea Asperti | Capturing Invalid_argument inside pp (otherwise we... |
tree | commitdiff |
| 2007-02-09 |
Claudio Sacerdoti... | Avoid generating invalid names with "'" in the middle... |
tree | commitdiff |
| 2007-02-06 |
Claudio Sacerdoti... | Incredible bug fixed in Fix and CoFix. The types of... |
tree | commitdiff |
| 2007-01-02 |
Enrico Tassi | added oblivion_universe and used it in paxck_coercions |
tree | commitdiff |
| 2006-12-29 |
Ferruccio Guidi | now we try two distinct depend files for compilation... |
tree | commitdiff |
| 2006-11-12 |
Claudio Sacerdoti... | The pretty printers in CicPp now have an optional ... |
tree | commitdiff |
| 2006-10-23 |
Claudio Sacerdoti... | CicUniv.UniverseInconsistency is no handled correcly. |
tree | commitdiff |
| 2006-09-21 |
Enrico Tassi | "21" -> "Implicit found" |
tree | commitdiff |
| 2006-09-14 |
Claudio Sacerdoti... | Bug fixed in pretty printing in new syntax of MutCases... |
tree | commitdiff |
| 2006-09-13 |
Claudio Sacerdoti... | 1. Some warnings about unused warning fixed (hopefully... |
tree | commitdiff |
| 2006-09-12 |
Claudio Sacerdoti... | Possible bug fixed (similar to the previous one, but... |
tree | commitdiff |
| 2006-09-12 |
Claudio Sacerdoti... | Bug fixed in the guarded_by_descructors function: in... |
tree | commitdiff |
| 2006-09-04 |
Enrico Tassi | BIG FAT COMMIT REGARDING COERCIONS: |
tree | commitdiff |
| 2006-09-04 |
Andrea Asperti | Bug fixing. If the inductive types do not occur in... |
tree | commitdiff |
| 2006-07-22 |
Enrico Tassi | matitaprover |
tree | commitdiff |
| 2006-07-18 |
Claudio Sacerdoti... | head_beta_reduce can now optionally perform delta reduc... |
tree | commitdiff |
| 2006-06-14 |
Stefano Zacchiroli | removed old debugging print |
tree | commitdiff |
| 2006-05-29 |
Claudio Sacerdoti... | Bug fixed in fresh_name_generator: the function used... |
tree | commitdiff |
| 2006-04-13 |
Claudio Sacerdoti... | Profiling code commented out. |
tree | commitdiff |
| 2006-04-03 |
Claudio Sacerdoti... | Useless code simplified out. |
tree | commitdiff |
| 2006-03-30 |
Claudio Sacerdoti... | Bug fixed: terms with a Cast used to raise assert false... |
tree | commitdiff |
| 2006-03-29 |
Claudio Sacerdoti... | Huge speed-up in conversion: the old conversion strateg... |
tree | commitdiff |
| 2006-03-29 |
Claudio Sacerdoti... | #### EXPERIMENTAL COMMIT #### |
tree | commitdiff |
| 2006-03-29 |
Claudio Sacerdoti... | Debugging code added. |
tree | commitdiff |
| 2006-03-29 |
Enrico Tassi | reverted the addition of _ to mistyped names |
tree | commitdiff |
| 2006-03-28 |
Enrico Tassi | more profiling and fixes for paramod |
tree | commitdiff |
| 2006-03-27 |
Claudio Sacerdoti... | Debugging code commented out. |
tree | commitdiff |
| 2006-03-27 |
Claudio Sacerdoti... | "Performance bug" fixed: I removed a whd in the does_no... |
tree | commitdiff |
| 2006-03-27 |
Claudio Sacerdoti... | Several "try ... with _ -> " specialized. |
tree | commitdiff |
| 2006-03-24 |
Claudio Sacerdoti... | Recently introduced bug fixed in the kernel: a stack... |
tree | commitdiff |
| 2006-03-24 |
Claudio Sacerdoti... | more error messages were on stdout :-( |
tree | commitdiff |
| 2006-03-24 |
Claudio Sacerdoti... | error message was printed on stdout |
tree | commitdiff |
| 2006-03-15 |
Enrico Tassi | more work for the release |
tree | commitdiff |
| 2006-02-14 |
Enrico Tassi | reverted orrible but correct syntax |
tree | commitdiff |
| 2006-02-14 |
Enrico Tassi | fixed syntax |
tree | commitdiff |
| 2006-02-03 |
Stefano Zacchiroli | - renamed ocaml/ to components/ |
tree | commitdiff |
|
projects / helm.git / history