|
About the Developing plugins category
|
|
1
|
331
|
February 12, 2019
|
|
Cannot Compile Ynot Library in CoqIDE
|
|
3
|
93
|
August 28, 2021
|
|
Ltac2: unfold
|
|
2
|
100
|
June 10, 2021
|
|
Ltac2: pose and exists
|
|
1
|
68
|
June 10, 2021
|
|
Ltac2: timeout tactic
|
|
0
|
101
|
May 30, 2021
|
|
Ltac2: distinguishing between tactics with the same `beginning` of the name
|
|
3
|
99
|
May 23, 2021
|
|
A guide to building your Coq libraries and plugins with Dune
|
|
29
|
3206
|
May 21, 2021
|
|
Ltac2: checking if an optional input variable is present
|
|
2
|
103
|
May 21, 2021
|
|
Ltac2: Function to match a variable with a type
|
|
3
|
106
|
May 10, 2021
|
|
How to properly configure the ML load path for ocaml packages in opam projects
|
|
7
|
374
|
November 18, 2020
|
|
Recommended resource for developing Coq plugin
|
|
3
|
312
|
November 5, 2020
|
|
Proofview.tactic to string or Pp.t
|
|
3
|
301
|
August 22, 2020
|
|
"Running" Proofview.tactic to see if it would succeed
|
|
1
|
241
|
August 21, 2020
|
|
Can you pass tactics to a plugin?
|
|
4
|
310
|
August 21, 2020
|
|
Real number without axiom
|
|
8
|
323
|
June 28, 2020
|
|
Converting an Ltac tactic to Proofview.tactic
|
|
1
|
261
|
May 30, 2020
|
|
How can an OCaml tactic return something else than unit?
|
|
1
|
291
|
April 29, 2020
|
|
How do I solve "no implementation available for ..."?
|
|
1
|
346
|
October 8, 2019
|
|
Get global environment from coq
|
|
0
|
329
|
September 23, 2019
|
|
Best way to obtain constrs free from de Bruijn indices?
|
|
4
|
388
|
July 31, 2019
|
|
Trouble adding a new definition to the environment in 8.9.1
|
|
3
|
441
|
July 24, 2019
|
