aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2020-08-24Bench: artifact logsGaëtan Gilbert
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
2020-08-24Perform a few tweaks to make the bench script work properly.Pierre-Marie Pédrot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
2020-08-24Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer ...coqbot
2020-08-24Merge PR #12832: Introduce GitHub Action to check for conflicts in PRs.coqbot
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence of...Pierre-Marie Pédrot
2020-08-24CI: stop testing 4.11+trunkGaëtan Gilbert
2020-08-24added numeral_notation to META.coq.inAli Caglayan
2020-08-23Merge PR #12851: Extraction: At declaration point of a global, use its declar...Maxime Dénès
2020-08-22Namegen.visible_ids: fixing what seems to be typos.Hugo Herbelin
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
2020-08-21Use a map function instead of a fold when freezing summaries.Pierre-Marie Pédrot
2020-08-21Add a heterogeneous map function over Dyn.Map.Pierre-Marie Pédrot
2020-08-21Add Actions to CI realm in CODEOWNERS.Théo Zimmermann
2020-08-21Introduce GitHub Action to check for conflicts in PRs.Théo Zimmermann
2020-08-21Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to be...Pierre-Marie Pédrot
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
2020-08-20Use properly fresh names for Scheme EqualityJasper Hugunin
2020-08-20Special commit to start benchmarking.Maxime Dénès
2020-08-20Adding change log for PR #12816.Hugo Herbelin
2020-08-20Quick fix to #12787 (injection anomaly due to inconsistent comp. of free vars).Hugo Herbelin
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
2020-08-20Modify Init/Specif.v to compile with -mangle-namesJasper Hugunin
2020-08-20Modify Init/Datatypes.v to compile with -mangle-names.Jasper Hugunin
2020-08-20Modify Init/Logic.v to compile with -mangle-names.Jasper Hugunin
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
2020-08-20[vernac] refine check for unresolved evarsEnrico Tassi
2020-08-20Adding overlays.Pierre-Marie Pédrot
2020-08-20Do not store the transparent state in delayed dnets.Pierre-Marie Pédrot
2020-08-20Dnets now consider axioms as being opaque for pattern recognition.Pierre-Marie Pédrot
2020-08-19Improve `make approve-output`Jason Gross
2020-08-19[coqchk] Look inside inner modules as wellJason Gross
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
2020-08-19Prefer eval_tactic_ist, which has error localisation, to interp_tactic.Hugo Herbelin
2020-08-19In tacinterp.ml, renaming eval_tactic into eval_tactic_ist to match the API.Hugo Herbelin
2020-08-19Merge PR #12856: Adding a mention of the JSON extraction in the documentation.coqbot
2020-08-19Merge PR #12709: Simplify hint pattern handlingMatthieu Sozeau
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
2020-08-19Add overlay.Pierre-Marie Pédrot
2020-08-19Replace Hints.head_constr_bound with Hints.head_bound.Pierre-Marie Pédrot
2020-08-19Simplify the computation of the head global for hint patterns.Pierre-Marie Pédrot
2020-08-19Ensure statically that Hint Extern comes with a pattern.Pierre-Marie Pédrot
2020-08-19Adding the example of bug #2904 into the test suite, and reorganising the tes...Martin Bodin
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
2020-08-19Merge PR #12822: Do not precompute hint dnets eagerlyMatthieu Sozeau
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
2020-08-19No more arithmetic directory test-suite.Hugo Herbelin
2020-08-19Merge PR #12774: Fixing tactic loc updating in #12223Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 12:11:10 +0000