aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2019-05-21Fixing a small bug in computing implicit arguments in (co-)fixpoints.Hugo Herbelin
2019-05-21Adding test for old bug fixed in 8.5 (wrong implicit arguments in fixpoint).Hugo Herbelin
2019-05-21Fixing an indentation in constrintern.ml.Hugo Herbelin
2019-05-21Merge PR #10144: Fix #9919: conversion functions are non-linearHugo Herbelin
2019-05-20Merge PR #9530: Remove `VtUnkown` classificationGaëtan Gilbert
2019-05-20Merge PR #10186: [CI/Azure/macOS] Target macOS version 10.11Gaëtan Gilbert
2019-05-20Merge PR #9873: Remove test file with Timeout that failed spuriously.Gaëtan Gilbert
2019-05-20Remove VtUnknown classificationMaxime Dénès
2019-05-20Remove Refine Instance Mode optionMaxime Dénès
2019-05-20Merge PR #10149: [refman] Misc fixes (indentation, whitespace, notation syntax)Théo Zimmermann
2019-05-19[refman] Document etransitivityClément Pit-Claudel
2019-05-19[refman] Fix up the grammar entry for field_defClément Pit-Claudel
2019-05-19[refman] Add a .. cmd:: header for Reserved Notation and Reserved InfixClément Pit-Claudel
2019-05-19[refman] Fix up the documentation of Instance and Existing InstanceClément Pit-Claudel
2019-05-19[refman] Misc fixes (indentation, whitespace, notation syntax)Clément Pit-Claudel
2019-05-19Merge PR #10184: A few nix-related updatesThéo Zimmermann
2019-05-19Merge PR #10143: Add dedicated syntax for alternatives (abc | def) in manual ...Théo Zimmermann
2019-05-19Merge PR #10190: Implicit Quantifiers recurse in continuation of let-inHugo Herbelin
2019-05-19Implicit Quantifiers recurse in continuation of let-inJasper Hugunin
2019-05-18Merge PR #10134: Simplify impargsHugo Herbelin
2019-05-17[CI/Azure/macOS] Target macOS version 10.11Vincent Laporte
2019-05-17[nix] Update reference to nixpkgsVincent Laporte
2019-05-17[Nix-ci] Update Unicoq patchVincent Laporte
2019-05-17[default.nix] Exclude the nix/ directory from sourcesVincent Laporte
2019-05-17[Nix-CI] Bignums no longer depends on camlp5Vincent Laporte
2019-05-16[refman] Introduce syntax for alternatives in notationsClément Pit-Claudel
2019-05-15Merge PR #10150: Handle tags shorter than "diff." without an exceptionGaëtan Gilbert
2019-05-15Merge PR #10151: Clean up the API for side-effectsGaëtan Gilbert
2019-05-15Merge PR #9905: [vm] x86_64 registersMaxime Dénès
2019-05-15Simplify the private constant API.Pierre-Marie Pédrot
2019-05-14Merge PR #8893: Moving evars_of_term from constr to econstrPierre-Marie Pédrot
2019-05-14Merge PR #10125: Allow run_tactic to return a value, remove hack from ltac2Pierre-Marie Pédrot
2019-05-14Merge PR #10136: [ltac2] Add primitive integersPierre-Marie Pédrot
2019-05-14Merge PR #10164: Add aucontext debug printerPierre-Marie Pédrot
2019-05-14Merge PR #10135: Make detyping robust w.r.t. indexed anonymous variablesPierre-Marie Pédrot
2019-05-14Abstract away the implementation of side-effects in Safe_typing.Pierre-Marie Pédrot
2019-05-14Reduce the attack surface of Opaqueproof.Pierre-Marie Pédrot
2019-05-14Merge PR #10145: Code cleanups in tacticsHugo Herbelin
2019-05-14Remove the sidecond_first flag of apply-related tactics.Pierre-Marie Pédrot
2019-05-14Remove the elimrename field from Tactics.eliminator.Pierre-Marie Pédrot
2019-05-14Code factorization in elim tactics.Pierre-Marie Pédrot
2019-05-14Overlay for value-returning run_tacticGaëtan Gilbert
2019-05-14Allow run_tactic to return a value, remove hack from ltac2Gaëtan Gilbert
2019-05-14Add aucontext debug printerGaëtan Gilbert
2019-05-14Merge PR #10152: Move last changelog entries for 8.10+beta1.Vincent Laporte
2019-05-13Handle tags shorter than "diff." without an exceptionJim Fehrle
2019-05-13Adding overlay for Equations.Hugo Herbelin
2019-05-13Passing evar_map to evars_of_term rather than expecting the term to be evar-nf.Hugo Herbelin
2019-05-13Moving Evd.evars_of_term from constr to econstr + consequences.Hugo Herbelin
2019-05-13Missing change entry for #9854.Théo Zimmermann
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-27 22:21:04 +0000