|
About the Developing plugins category
|
|
0
|
809
|
February 10, 2019
|
|
Using vsrocq language server with Emacs
|
|
3
|
108
|
November 13, 2026
|
|
Tuareg-mode doesn't really work for mlg file
|
|
1
|
100
|
December 20, 2025
|
|
Any good resources on extracting Coq to other languages?
|
|
0
|
112
|
May 18, 2025
|
|
Figuring out How Rocq Imports Affect the names available to Smartlocate.global_alias_* calls in an OCaml Plugin
|
|
3
|
111
|
February 14, 2025
|
|
Best way to deal with mlg files warning-as-errors in plugins built by dune?
|
|
3
|
212
|
June 22, 2024
|
|
Learning to write Coq plugins - what is the purpose of .mlg files?
|
|
5
|
288
|
June 7, 2024
|
|
Coq Plugin to output hypotheses, goal and tactic in JSON
|
|
4
|
344
|
May 11, 2024
|
|
Proof of Concept in getting COQ running inside of LLama.cpp, need help
|
|
2
|
554
|
December 12, 2023
|
|
Is there a way to extract ASTs from the Coq compiler?
|
|
2
|
613
|
June 15, 2023
|
|
A guide to building your Coq libraries and plugins with Dune
|
|
35
|
8598
|
April 29, 2023
|
|
How does one access the dependent type unification algorithm from Coq's internals -- especially the one from apply and the substitution solution?
|
|
0
|
574
|
July 13, 2022
|
|
What are Generic Arguments in Coq and how are they structured in their OCaml code?
|
|
0
|
697
|
July 14, 2022
|
|
How to evaluate proof terms through opaque definitions?
|
|
0
|
737
|
May 30, 2022
|
|
Cannot Compile Ynot Library in CoqIDE
|
|
4
|
779
|
May 12, 2022
|
|
Calling Coq from OCaml
|
|
1
|
877
|
April 22, 2022
|
|
Ltac2: unfold
|
|
2
|
854
|
June 10, 2021
|
|
Ltac2: pose and exists
|
|
1
|
792
|
June 10, 2021
|
|
Ltac2: timeout tactic
|
|
0
|
738
|
May 30, 2021
|
|
Ltac2: distinguishing between tactics with the same `beginning` of the name
|
|
3
|
958
|
May 23, 2021
|
|
Ltac2: checking if an optional input variable is present
|
|
2
|
659
|
May 21, 2021
|
|
Ltac2: Function to match a variable with a type
|
|
3
|
878
|
May 10, 2021
|
|
How to properly configure the ML load path for ocaml packages in opam projects
|
|
7
|
1622
|
November 18, 2020
|
|
Recommended resource for developing Coq plugin
|
|
3
|
1017
|
November 5, 2020
|
|
Proofview.tactic to string or Pp.t
|
|
3
|
908
|
August 22, 2020
|
|
"Running" Proofview.tactic to see if it would succeed
|
|
1
|
752
|
August 21, 2020
|
|
Can you pass tactics to a plugin?
|
|
4
|
1064
|
August 21, 2020
|
|
Real number without axiom
|
|
8
|
1306
|
June 28, 2020
|
|
Converting an Ltac tactic to Proofview.tactic
|
|
1
|
722
|
May 30, 2020
|
|
How can an OCaml tactic return something else than unit?
|
|
1
|
754
|
April 29, 2020
|