aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2016-02-15Code factorization of tactic "unfold_body".Pierre-Marie Pédrot
2016-02-15More conversion functions in the new tactic API.Pierre-Marie Pédrot
2016-02-15Moving conversion functions to the new tactic API.Pierre-Marie Pédrot
2016-02-15Renaming functions in Typing to stick to the standard e_* scheme.Pierre-Marie Pédrot
2016-02-15Monotonizing the Evarutil module.Pierre-Marie Pédrot
2016-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2016-02-13Do not give a name to anonymous evars anymore. See bug #4547.Pierre-Marie Pédrot
2016-02-10STM: always stock in vio files the first node (state) of a proofEnrico Tassi
2016-02-10STM: not delegate proofs that contain Vernac(Module|Require|Import), #4530Enrico Tassi
2016-02-10Don't fail fatally if PATH is not set.Emilio Jesus Gallego Arias
2016-02-08Improving error message with missing patterns in the presence ofHugo Herbelin
2016-02-03Optimizing the universes_of_constr_function.Pierre-Marie Pédrot
2016-02-03Optimizing the computation of frozen evars.Pierre-Marie Pédrot
2016-02-03Adding a "get" primitive to map signature.Pierre-Marie Pédrot
2016-02-03Opacifying the type of evar naming structure in Evd.Pierre-Marie Pédrot
2016-02-03More compact representation for evar resolvability flag.Pierre-Marie Pédrot
2016-02-02Removing a source of type-unsafeness in Pcoq.Pierre-Marie Pédrot
2016-02-01Infering atomic ML entries from their grammar.Pierre-Marie Pédrot
2016-01-29Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-27Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Pierre-Marie Pédrot
2016-01-26Fixing bde12b70 about reporting ill-formed constructor.Hugo Herbelin
2016-01-24Tentative fix for bug #4522: Incorrect "Warning..." on windows.Pierre-Marie Pédrot
2016-01-24Fixing bug #4373: coqdep does not know about .vio files.Pierre-Marie Pédrot
2016-01-24Fixing bug #3826: "Incompatible module types" is uninformative.Pierre-Marie Pédrot
2016-01-24Adding a test for bug #4378.Pierre-Marie Pédrot
2016-01-24Fixing bug #4495: Failed assertion in metasyntax.ml.Pierre-Marie Pédrot
2016-01-24Fixing bug #4511: evar tactic can create non-typed evars.Pierre-Marie Pédrot
2016-01-23Fix bug #4503: mixing universe polymorphic and monomorphicMatthieu Sozeau
2016-01-23Fix bug #4519: oops, global shadowed local universe level bindings.Matthieu Sozeau
2016-01-23Implement support for universe binder lists in Instance and Program Fixpoint/...Matthieu Sozeau
2016-01-23Fix bug #4506. Using betadeltaiota_nolet might produce terms of the formMatthieu Sozeau
2016-01-22Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.Hugo Herbelin
2016-01-22Restore warnings produced by the interpretation of the command lineHugo Herbelin
2016-01-21New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Hugo Herbelin
2016-01-21Compile OS X binaries without native_compute support.Maxime Dénès
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-21Stronger invariants on the use of the introduction pattern (pat1,...,patn).Hugo Herbelin
2016-01-21Fixing some problems with double induction.Hugo Herbelin
2016-01-20Code simplification in elim.ml.Hugo Herbelin
2016-02-18Fixing a bug with introduction patterns over inductive types containing let-ins.Hugo Herbelin
2016-01-20Update cic.mli MD5 after header update.Maxime Dénès
2016-01-20Update version number in configure.Maxime Dénès
2016-01-20Update copyright headers.Maxime Dénès
2016-01-20Change $(...)$ to ltac:(...) in section 2.11. Fixes #4500.Maxime Dénès
2016-01-20Documenting Set Bullet Behavior.Hugo Herbelin
2016-01-20Clarifying the documentation of tactics "cbv" and "lazy".Hugo Herbelin
2016-01-20Fixing Not_found on unknown bullet behavior.Hugo Herbelin
2016-01-19Fix bug #4420: check_types was losing universe constraints.Matthieu Sozeau
2016-01-17Universes algorithm : clarified commentsJacques-Henri Jourdan
2016-01-17Moving val_cast to Tacinterp.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 14:23:37 +0000