aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2020-08-25Merge PR #12778: Merging is now possible with coqbot.coqbot-app[bot]
Reviewed-by: ejgallego
2020-08-25Merge PR #12878: Update sigma instead of erasing it in `update_global_env`coqbot-app[bot]
Reviewed-by: SkySkimmer
2020-08-24Merge PR #12886: Fix Coqtail test directory.Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-08-24Fix Coqtail test directory.whonore
Tests moved in https://github.com/whonore/Coqtail/pull/134.
2020-08-24Merge PR #12868: Lint stdlib with -mangle-names #1Anton Trunov
Reviewed-by: anton-trunov
2020-08-24Merge PR #12835: Slightly reorganising the test suite to follow its ↵Hugo Herbelin
documentation Reviewed-by: SkySkimmer Reviewed-by: herbelin Reviewed-by: jfehrle
2020-08-24Merge PR #12565: Dnets now consider axioms as being opaque for pattern ↵coqbot
recognition. Reviewed-by: mattam82
2020-08-24Update sigma instead of erasing it in `update_global_env`Maxime Dénès
2020-08-24Merge PR #12738: Fix subject reduction VS cumulative inductives and function etacoqbot
Reviewed-by: mattam82 Ack-by: ppedrot
2020-08-24Merge PR #12864: Improve `make approve-output`Gaëtan Gilbert
Reviewed-by: SkySkimmer
2020-08-24Merge PR #12854: Mini-fix in test suite: arithmetic directory does no longer ↵coqbot
exist Reviewed-by: SkySkimmer
2020-08-24Merge PR #12832: Introduce GitHub Action to check for conflicts in PRs.coqbot
Reviewed-by: SkySkimmer
2020-08-24Merge PR #12816: Fixes #12787: anomaly of tactic injection in the presence ↵Pierre-Marie Pédrot
of artificial dependencies disappearing by reduction Reviewed-by: ppedrot
2020-08-23Merge PR #12851: Extraction: At declaration point of a global, use its ↵Maxime Dénès
declaring name Reviewed-by: maximedenes
2020-08-22Merge PR #12866: Less fragile scheme equalityHugo Herbelin
Ack-by: SkySkimmer Reviewed-by: herbelin
2020-08-21Merge PR #12853: Another tactic error location fix after PR#12223 and PR#12774Pierre-Marie Pédrot
Reviewed-by: ppedrot
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
Alternative to adding this feature to coqbot (coq/bot#14).
2020-08-21Merge PR #12857: [ssr] when porting v8.2 code no backtracking point has to ↵Pierre-Marie Pédrot
be added Reviewed-by: CohenCyril Reviewed-by: ppedrot
2020-08-21Merge PR #12759: [vernac] refine check for unresolved evarscoqbot
Reviewed-by: SkySkimmer Ack-by: gares
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
We fix it by reducing K-redexes the same in the both places (make_tuple and minimal_free_rels) which compute the dependencies of a dependent equality.
2020-08-20[ssr] when porting v8.2 code no backtracking point has to be addedEnrico Tassi
Amends c1b1afe76e1655cc3275bdf4215f0ab690efc3cc
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
All except `pair_equal_spec` completely addressed by moving dependent hypotheses before the colon.
2020-08-20Modify Init/Logic.v to compile with -mangle-names.Jasper Hugunin
This is related to coq/coq#6781. Most issues are with `destruct H` where H is the name of a binder in the goal; this is addressed by moving dependent assumptions before the colon. A different option would be adding `intros` tactics, but this repeats the names of hypotheses (in the type of the goal and in the proof script). Additionally, the `destruct H with (Q:=...)` form gets changed to `destruct (H ...)`, since the binder name `Q` is refreshed.
2020-08-20Merge PR #12756: Do not refresh the names of implicit arguments.Maxime Dénès
Reviewed-by: herbelin Reviewed-by: maximedenes
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
We know statically that it is going to be the one provided at the time of lookup, so we simply fetch it from there.
2020-08-20Dnets now consider axioms as being opaque for pattern recognition.Pierre-Marie Pédrot
2020-08-19Improve `make approve-output`Jason Gross
It now silently does nothing rather than erroring with `mv: cannot stat 'output/*.out.real': No such file or directory` if there is no output to approve, and also correctly handles `output-coqtop` and `output-coqchk` rather than ignoring these directories. Fixes #12863
2020-08-19Yet other tactic error location fixes (see PR#12223 and PR#12774).Hugo Herbelin
When calling an Ltac function, add specific locations when interpreting the function, when interpreting the arguments and when executating the call (in a TacArg).
2020-08-19Prefer eval_tactic_ist, which has error localisation, to interp_tactic.Hugo Herbelin
This is important for TacArg arguments, which typically corresponds to calling an Ltac function.
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
Reviewed-by: jfehrle
2020-08-19Merge PR #12709: Simplify hint pattern handlingMatthieu Sozeau
Reviewed-by: mattam82
2020-08-19Do not refresh the names of implicit arguments.Jasper Hugunin
Try just going with the user-given names, and not worrying about what happens with repeated names or anonymous implicits. (Support for anonymous implicits is due to herbelin in #11098.) This PR should not change behaviour in the absence of repeated names. Since repeated names are already a poorly handled corner case, I would recommend changing binder names to avoid overlap in the case of a change in behavior. Since anonymous implicits and implicits with repeated names can already happen, I think this is unlikely to cause too many new problems, though it might exacerbate existing ones. However, I already had to fix one newly possible anomaly, so I can't be too confident. The most common change in external developments was that an argument no longer gets `0` appended to it, causing the `Arguments` command to complain about renaming. To fix this and keep the old name, one can simply use the `rename` flag as suggested, or switch to the new, un-suffixed name. Closes #6785 Closes #12001 Another step towards checking the standard library with `-mangle-names`.
2020-08-19Add overlay.Pierre-Marie Pédrot
2020-08-19Replace Hints.head_constr_bound with Hints.head_bound.Pierre-Marie Pédrot
The two implementations are essentially the same except for potential interleaving of let-bindings and pattern-matchings. The only place the removed function was called probably does not rely on this difference of behaviour.
2020-08-19Simplify the computation of the head global for hint patterns.Pierre-Marie Pédrot
Instead of having to go through the pattern translation, we compute the pattern directly from the term.
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 ↵Martin Bodin
test files. Co-authored-by: Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> Co-authored-by: Hugo Herbelin <Hugo.Herbelin@inria.fr>
2020-08-19Fixes #10902 by adding a mention of the JSON extraction in the documentation.Martin Bodin
Co-authored-by: Jim Fehrle <jim.fehrle@gmail.com>
2020-08-19Merge PR #12822: Do not precompute hint dnets eagerlyMatthieu Sozeau
Reviewed-by: mattam82
2020-08-19Merge PR #12725: Store evar identity instances in evarinfo / named_context_valEnrico Tassi
Ack-by: SkySkimmer Reviewed-by: gares
2020-08-19No more arithmetic directory test-suite.Hugo Herbelin
The directory is obsolete since 7461fe4f.
2020-08-19Merge PR #12774: Fixing tactic loc updating in #12223Pierre-Marie Pédrot
Reviewed-by: ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-08 22:54:36 +0000