aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-10-19Function debug mode more formatted.Pierre Courtieu
2015-10-19Partly fixes #3225. Removed some old experimental stuff in funind.Pierre Courtieu
2015-10-19Fixed #4274, bad formatting of messages in emacs mode.Pierre Courtieu
2015-10-19Documenting the option "Strict Universe Declaration" in CHANGES.Pierre-Marie Pédrot
2015-10-18Making Evarutil.new_evar monotonous.Pierre-Marie Pédrot
2015-10-18Constraining refine to monotonic functions.Pierre-Marie Pédrot
2015-10-18Miscellaneous typos, spacing, US spelling in comments or variable names.Hugo Herbelin
2015-10-18Using "__" rather than this unelegant arbitrary "A" for the name of variables...Hugo Herbelin
2015-10-18Reference Manual: Applying standard style recommendation about notHugo Herbelin
2015-10-18Fixing #4198 (continued): not matching within the inner lambdas/let-insHugo Herbelin
2015-10-18Using appropriate lambda decomposition function counting let-ins whenHugo Herbelin
2015-10-18Adding a function to mirror decompose_prod_n_assum in that it counts let-ins,Hugo Herbelin
2015-10-18Adding a notion of monotonous evarmap.Pierre-Marie Pédrot
2015-10-17Clarifying and documenting the UState API.Pierre-Marie Pédrot
2015-10-17Dedicated file for universe unification context manipulation.Pierre-Marie Pédrot
2015-10-17Lemmas accept the Local flag.Pierre-Marie Pédrot
2015-10-17Test for bug #4325.Pierre-Marie Pédrot
2015-10-16Generalize fix for auto from PMP to eauto and typeclasses eauto.Matthieu Sozeau
2015-10-16Merge branch 'v8.5' into trunkMaxime Dénès
2015-10-16Hashcons bytecode generated by the VM.Pierre-Marie Pédrot
2015-10-16Exporting a purely functional interface to bytecode patching.Pierre-Marie Pédrot
2015-10-16Remove left2right reference from the kernel.Maxime Dénès
2015-10-16Merge hint lists instead of appending them. (Fix bug #3199)Guillaume Melquiond
2015-10-15Avoid dependency of the pretyper on C code.Maxime Dénès
2015-10-15Test file for #4346: Set is no longer of type TypeMaxime Dénès
2015-10-15 Fix #4346 2/2: VM casts were not inferring universe constraints.Maxime Dénès
2015-10-15Fix #4346 1/2: native casts were not inferring universe constraints.Maxime Dénès
2015-10-15Warn user when bytecode compilation fails.Maxime Dénès
2015-10-15Remove now useless exception handler in default conversion.Maxime Dénès
2015-10-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-10-15Fix detection of ties in oracle_order.Guillaume Melquiond
2015-10-14Reverting modifications in dev/top_printers pushed mistakenly.Pierre-Marie Pédrot
2015-10-14Fixing perfomance issue of auto hints induced by universes.Pierre-Marie Pédrot
2015-10-14Fix LemmaOverloadingMatthieu Sozeau
2015-10-14Occur-check in evar_define was not strong enough.Matthieu Sozeau
2015-10-14Fix constr_matching when a match is found in the head of a case constructMatthieu Sozeau
2015-10-14When typechecking a lemma statement, try to resolve typeclasses beforeMatthieu Sozeau
2015-10-14Univs: inductives, remove unneeded testMatthieu Sozeau
2015-10-14Temporary fix: kernel conversion needs to ignore l2r flag.Maxime Dénès
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-10-14Fixing evarmap implementation.Pierre-Marie Pédrot
2015-10-14Remove reference to default conversion function inside the kernel.Maxime Dénès
2015-10-14Remove -vm flag of coqtop.Maxime Dénès
2015-10-14Remove unused infos structure in VM.Maxime Dénès
2015-10-14Fixing bug #4367: Wrong error message in unification.Pierre-Marie Pédrot
2015-10-14Make interpreter of PROJ simpler by not using the stack.Guillaume Melquiond
2015-10-14Remove some unused variables.Guillaume Melquiond
2015-10-14Fix some typos.Guillaume Melquiond
2015-10-13Fix some typos.Guillaume Melquiond
2015-10-12Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 11:15:05 +0000