]> matita.cs.unibo.it Git - helm.git/history - helm/software/components/cic_proof_checking
\ldots are now used in nelim and ncases
[helm.git] / helm / software / components / cic_proof_checking /
2009-07-07 Claudio Sacerdoti... 1) Include files for NG were neither recursively proces...
2009-06-25 Ferruccio Guidi- some depend files :)
2009-06-15 Enrico Tassihuge commit regarding the grafite_status:
2009-06-03 Claudio Sacerdoti... Huge commit with several changes:
2009-05-18 Enrico Tassinothing special
2009-05-15 Claudio Sacerdoti... Patch to add a debugging string to HExtlib.split_nth...
2009-05-14 Ferruccio Guidi- hExtlib: added debugging information for split_nth
2009-05-08 Claudio Sacerdoti... ...
2009-04-14 Ferruccio Guidiwe rebuilt the dependences
2009-03-25 Enrico Tassinew tactics are almost ready
2009-02-05 Enrico Tassia non necessary but morally required change. The matche...
2009-02-02 Enrico TassiCicTypeChecker.typecheck now takes an additional parameter:
2009-01-29 Enrico Tassiapplication arguments are compared with test_eq_only...
2009-01-13 Enrico Tassimany changes regarding coercions:
2008-12-19 Enrico Tassi...
2008-11-28 Ferruccio GuidicicDischarge: final fixup. Now correctly processes...
2008-11-28 Ferruccio Guiding_disambiguation ng_kernel ng_refiner disambiguation...
2008-11-27 Enrico Tassi1. grafiteDisambiguator => multiPassDisambiguator
2008-11-25 Ferruccio GuidicicUtil: we moved here pp_term from proceduralHelpers
2008-10-13 Claudio Sacerdoti... Bug fixed in LetIn: the cumulativity test was performed...
2008-09-10 Ferruccio GuidicicDischarge, Procedural: we improved debugging and...
2008-09-07 Ferruccio GuidicicDischarge: we still have some problems here. Some...
2008-08-28 Ferruccio GuidicicDischarge: new module for discharging the explicit...
2008-08-01 Enrico Tassifixed recursiveness check
2008-07-30 Enrico Tassifixed check, if 0 constructors then no List.nth is...
2008-07-30 Enrico Tassiallowed sort elim now check for recursive types
2008-07-30 Claudio Sacerdoti... Missing check implemented: uniformity of left parameter...
2008-07-23 Enrico Tassipositivity check fixed, some subterms were erroneously...
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...
next