Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Coq 8.19 #702

Merged
merged 40 commits into from
Feb 8, 2024
Merged
Changes from 1 commit
Commits
Show all changes
40 commits
Select commit Hold shift + click to select a range
35e54a2
Test against Coq's master
maximedenes Aug 21, 2023
b57c98a
Fix Nix build
maximedenes Aug 21, 2023
a3b3956
Adapt to coq/coq#17928 (Search uses search_restriction instead of bool)
SkySkimmer Aug 9, 2023
6eda154
Merge pull request #564 from SkySkimmer/search-restr
maximedenes Aug 21, 2023
5ee2ad4
Adapt to Coq PR #17987 which adds sigma to the API of search functions
herbelin Aug 30, 2023
b0be276
Merge pull request #601 from herbelin/coq-master+adapt-coq-pr17987-se…
rtetley Sep 8, 2023
de88278
Adapt to Coq PR #18007: Proof_using.definition_using takes names of r…
herbelin Oct 8, 2023
4e6a855
Adapt to Coq PR #18007: Proof_using.definition_using takes names of r…
herbelin Oct 8, 2023
5f750ad
Adapt to https://github.com/coq/coq/pull/14928
proux01 Oct 9, 2023
d2b3249
Merge pull request #654 from herbelin/coq-master+adapt-coq-pr18007-ex…
SkySkimmer Oct 24, 2023
b3a7ed9
Adapt to coq/coq#18187 (reductionbehaviour is on constant not globref)
SkySkimmer Oct 24, 2023
e2ac4a9
Merge pull request #680 from SkySkimmer/redbehaviour-pred
SkySkimmer Oct 26, 2023
52e93f5
Adapt w.r.t. coq/coq#17136.
ppedrot Nov 6, 2023
fd291f5
Merge pull request #685 from ppedrot/stream_error_to_gramlib
ppedrot Nov 9, 2023
907bed4
Merge pull request #681 from coq-community/coq_14928
ppedrot Nov 10, 2023
a1aa8fe
Adapt w.r.t. coq/coq#18312.
ppedrot Nov 15, 2023
84032c7
Merge pull request #688 from ppedrot/detuplify-impargs
SkySkimmer Nov 16, 2023
d8a72d9
[wip] Merge branch 'coq-master' into coq-8.19
gares Dec 24, 2023
0dba89a
[ci] opam: test 8.18 and 8.19
gares Dec 24, 2023
215b5e1
[ppx_optcomp] define coq version
gares Dec 24, 2023
3e737ce
[wip] ifdef for 8.18
gares Dec 24, 2023
ca7733b
downgrade dune, there is an error with lang dune 3.5
gares Dec 24, 2023
1c3e1f2
Update .github/workflows/ci.yml
gares Dec 24, 2023
58a8df2
Update .github/workflows/ci.yml
gares Dec 24, 2023
9284071
Update language-server/build-windows-platform.bat
gares Dec 24, 2023
9c8a869
fixup ci
gares Dec 24, 2023
3a9f229
fix ci opam
gares Dec 24, 2023
466e732
progress
gares Dec 24, 2023
355e0dd
fix more code
gares Dec 25, 2023
f40ef29
more fix
gares Dec 25, 2023
e1e89f4
Update language-server/dm/executionManager.ml
gares Dec 29, 2023
c8f063f
Updating nix flakes
rtetley Jan 30, 2024
97d0fc5
Merge branch 'main' into coq-8.19
rtetley Jan 31, 2024
8878774
fixing deps. wip
rtetley Jan 31, 2024
4b986bf
Fixing nix.
rtetley Feb 2, 2024
9b99cb6
Nix build for different coq versions.
rtetley Feb 5, 2024
87dd6d0
Fix typo in flake
rtetley Feb 5, 2024
bf063d8
Fix flake + adapt to https://github.com/coq/coq/pull/18529
rtetley Feb 6, 2024
cd0d767
Update .github/workflows/ci.yml
rtetley Feb 6, 2024
bf48804
Update .github/workflows/ci.yml
gares Feb 6, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
Adapt to coq/coq#14928
proux01 committed Oct 9, 2023
commit 5f750adfef88ab34a93c38842bee79078f6a21a7
14 changes: 10 additions & 4 deletions language-server/language/hover.ml
Original file line number Diff line number Diff line change
@@ -40,7 +40,11 @@ let compactify s =
(* TODO this should be exposed by Coq and removed from here *)
let pr_args args more_implicits mods =
let open Vernacexpr in
let pr_s = prlist (fun CAst.{v=s} -> str "%" ++ str s) in
let pr_delimiter_depth = function
| Constrexpr.DelimOnlyTmpScope -> str "%_"
| Constrexpr.DelimUnboundedScope -> str "%" in
let pr_scope_delimiter (d, sc) = pr_delimiter_depth d ++ str sc in
let pr_s = prlist (fun CAst.{v=s} -> pr_scope_delimiter s) in
let pr_if b x = if b then x else str "" in
let pr_one_arg (x,k) = pr_if k (str"!") ++ Name.print x in
let pr_br imp force x =
@@ -57,7 +61,9 @@ let pr_args args more_implicits mods =
else
let rec fold extra = function
| RealArg arg :: tl when
List.equal (fun a b -> String.equal a.CAst.v b.CAst.v) arg.notation_scope s
List.equal
(fun a b -> let da, a = a.CAst.v in let db, b = b.CAst.v in
da = db && String.equal a b) arg.notation_scope s
&& arg.implicit_status = imp ->
fold ((arg.name,arg.recarg_like) :: extra) tl
| args -> List.rev extra, args
@@ -131,7 +137,7 @@ let rec main_implicits i renames recargs scopes impls =
| [], (None::_ | []) -> (Anonymous, Glob_term.Explicit)
in
let notation_scope = match scopes with
| scope :: _ -> List.map CAst.make scope
| scope :: _ -> List.map (fun s -> CAst.make (Constrexpr.DelimUnboundedScope, s)) scope
| [] -> []
in
let status = {Vernacexpr.implicit_status; name; recarg_like; notation_scope} in
@@ -260,4 +266,4 @@ let get_hover_contents env sigma ref_or_by_not =
end
in
Option.map Lsp.Types.(fun value -> MarkupContent.create ~kind:MarkupKind.Markdown ~value) r
| Constrexpr.ByNotation (_ntn,_sc) -> assert false
| Constrexpr.ByNotation (_ntn,_sc) -> assert false