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