aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2015-09-10fresh now accepts more things than just identifiers.Pierre Courtieu
2015-09-09Merge remote-tracking branch 'origin/v8.5' into trunkHugo Herbelin
2015-09-08Emphasizing that eta for vectors is an instance of caseS, as pointedHugo Herbelin
2015-09-08Fixing incomplete bugfix in 76f27140e6e34 (unfortunately 5 commitsHugo Herbelin
2015-09-08Minor modifications to WeakFanTheorem.Hugo Herbelin
2015-09-08Ensuring that patterns of the form pat/constr move the hypotheses replacingHugo Herbelin
2015-09-08Short cosmetic changes in tactics.ml.Hugo Herbelin
2015-09-08A bit of documentation of OCaml code for intro_patterns.Hugo Herbelin
2015-09-08New option "Unset Bracketing Last Introduction Pattern" for preservingHugo Herbelin
2015-09-08Fixing clearing of temporary hypotheses with intro pattern pat/constr.Hugo Herbelin
2015-09-08Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposedHugo Herbelin
2015-09-08Hacking parser so as to support both [> ... ] and [id].Hugo Herbelin
2015-09-08Adding a proof of eta on Vector.t of non-zero size.Hugo Herbelin
2015-09-08Documenting the code when preference is given to expansion of defaultHugo Herbelin
2015-09-08Documenting the new behaviour of the Shrink Obligations flag.Pierre-Marie Pédrot
2015-09-08All Program obligations now respect the Shrink Obligation flag.Pierre-Marie Pédrot
2015-09-08More potentialities in proof_terminators.Pierre-Marie Pédrot
2015-09-08Opacifying the proof_terminator type.Pierre-Marie Pédrot
2015-09-08Fixing the Shrink Obligations option.Pierre-Marie Pédrot
2015-09-06Merge branch 'v8.5' into trunkMaxime Dénès
2015-09-06Output a warning when conversion compilation failed.Maxime Dénès
2015-09-06Fix a bug in 31 bit arithmetic, leading to failing conversion tests.Maxime Dénès
2015-09-06Fixed critical bug in 31 bit arithmetic of VMCatalin Hritcu
2015-09-06Merge branch 'v8.5'Pierre-Marie Pédrot
2015-09-06Adding a Makefile target for the MSets and MMaps directories.Pierre-Marie Pédrot
2015-09-03Update test-suite after 518049fe7.Maxime Dénès
2015-09-03print universes when dumping bytecode.Gregory Malecha
2015-09-03Improve directives for Haskell extraction of nat.Maxime Dénès
2015-09-03Fix [Z.div] and add [Z.modulo] in ExtrHaskellZNum.vNickolai Zeldovich
2015-09-03Fix [Nat.div] and add [Nat.modulo] in ExtrHaskellNatNum.vNickolai Zeldovich
2015-09-03Implementing Herbelin's fix for the "NonPar" bugmlasson
2015-09-03Also there's an extra space in the error message.mlasson
2015-09-03Add an if_verbose for "Fetching opaque proofs ..."mlasson
2015-09-03Missing argument "-c" for coqdep in coq_makefilemlasson
2015-09-01STM: save a full state for queries.Enrico Tassi
2015-08-31Switching to an event-based mechanism for CoqIDE preferences.Pierre-Marie Pédrot
2015-08-29Adding a proof of surjective pairing on vectors.Hugo Herbelin
2015-08-29Fixing generation of dev/printers.mllib.d after ocamllibdep is used (48d611ff...Hugo Herbelin
2015-08-26Replacing old-style preferences in CoqIDE.Pierre-Marie Pédrot
2015-08-22Code cleaning in Obligations.Pierre-Marie Pédrot
2015-08-22Documenting the Shrink Abstract option.Pierre-Marie Pédrot
2015-08-22Allowing the abstract tactical to clear the environment from unused variables.Pierre-Marie Pédrot
2015-08-22Merge branch 'v8.5'Pierre-Marie Pédrot
2015-08-21Fixing #4318 (anomaly when applying args to a recursive notation in patterns).Hugo Herbelin
2015-08-19Removing code duplication in Lemmas.Pierre-Marie Pédrot
2015-08-19Documentation by giving a name to a large type.Pierre-Marie Pédrot
2015-08-17Highlighting of the "Next Obligation" command in CoqIDE.Pierre-Marie Pédrot
2015-08-17windows build scripts made more accurate in detecting failuresEnrico Tassi
2015-08-17Remove duplicate code.Guillaume Melquiond
2015-08-17Remove generatable documentation files from repository. (Fix bug #4315)Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-04 21:29:48 +0000