coq
forked from coq/coq
Star 1
Fork 0
Watch

Version history of engine/proofview.ml

August 2026

coqbot-app[bot]
Merge PR #22013: Simplifications in logic_monad
committed

July 2026

Gaëtan Gilbert
tclCASE use result instead of adhoc type
committed
Gaëtan Gilbert
Simplify list_view / reified types in logic_monad
committed
Gaëtan Gilbert
Logic_monad split returns result
committed

June 2026

coqbot-app[bot]
Merge PR #21987: Keep track of which variables are section variables and use this info to fix bugs
committed

May 2026

Gaëtan Gilbert
Keep track of variable status (secvar or not) in named contexts
committed
coqbot-app[bot]
Merge PR #17266: Command modifier and tactic for allocation limits
committed

April 2026

Gaëtan Gilbert
Experiment: command modifier and tactic for allocation limits
committed

March 2026

coqbot-app[bot]
Merge PR #21737: Renamings, cleanup and UState.from_uctx which respects invariants
committed
Yann Leray
Rename evar_universe_context into ustate
committed
coqbot-app[bot]
Merge PR #21793: Faster fast path for progress failure
committed
Gaëtan Gilbert
Faster fast path for progress failure
committed

January 2026

coqbot-app[bot]
Merge PR #21546: Improve error message for tactic timeout
committed
coqbot-app[bot]
Merge PR #21247: Collapse NonLogical thunks in the logic monad.
committed
Gaëtan Gilbert
Improve error message for tactic timeout
committed

December 2025

coqbot-app[bot]
Merge PR #21366: Manipulate lists rather than qualified identifiers in Evarnames.
committed
Pierre-Marie Pédrot
Take a qualid in Evarnames.resolve.
committed
Pierre-Marie Pédrot
Manipulate lists rather than qualified identifiers in Evarnames.
committed

November 2025

Pierre-Marie Pédrot
Bake the NonLogical run in Logic_monad.run.
committed
coqbot-app[bot]
Merge PR #21304: Clean up APIs and implementations around tclABSTRACT
committed
Pierre-Marie Pédrot
Remove Proofview.tclEFFECTS altogether.
committed
Pierre-Marie Pédrot
Remove dead API around Evd.side_effects.
committed
Pierre-Marie Pédrot
Simplify the implementation of tclEFFECTS.
committed
coqbot-app[bot]
Merge PR #21284: Reimplement abstract in a purely functional way.
committed
Pierre-Marie Pédrot
Reimplement abstract in a purely functional way.
committed

October 2025

coqbot-app[bot]
Merge PR #21149: Properly handle `Timeout x Fail cmd`
committed
Gaëtan Gilbert
Cleanup backtrace handling in timeout implementation
committed

May 2025

coqbot-app[bot]
Merge PR #20617: Ensure that Proofview.focus_context returns undefined evars
committed
coqbot-app[bot]
Merge PR #20600: Fix missing implicit name from notation ToPostHole
committed
Pierre-Marie Pédrot
Ensure that Proofview.focus_context returns undefined evars.
committed
Gaëtan Gilbert
Evar kind ImplicitArg always contains an ident
committed
coqbot-app[bot]
Merge PR #20511: Extend goal selection to allow multiple named goals
committed
Dario Halilovic
Remove partition_map
committed
Dario Halilovic
Use CSig.union instead of options
committed
Dario Halilovic
Make CList.partition_map available for OCaml version < 4.12
committed
Dario Halilovic
Add NthSelector to fix failing test case
committed
Dario Halilovic
Accept named goals in selector lists
committed

April 2025

coqbot-app[bot]
Merge PR #20472: Clean some bits of code related to side-effects
committed
Pierre-Marie Pédrot
Return the environment in Proofview.apply and callers.
committed

February 2025

coqbot-app[bot]
Merge PR #20132: Evd.new_pure_evar relevance argument is required instead of guessing Relevant
committed

January 2025

Gaëtan Gilbert
Evd.new_pure_evar relevance argument is required instead of guessing Relevant
committed
coqbot-app[bot]
Merge PR #20026: Rename Coq -> Rocq in various comments and doc
committed
Pierre Roux
Rename Coq -> Rocq in various comments and doc
committed

October 2024

coqbot-app[bot]
Merge PR #19692: Update the OCaml headers to reflect the fact Coq is now Rocq.
committed
Pierre-Marie Pédrot
Update the OCaml headers to reflect the fact Coq is now Rocq.
committed

September 2024

coqbot-app[bot]
Merge PR #19545: Add profiling entries around `abstract` sub-operations
committed
Gaëtan Gilbert
Add profiling entries around `abstract` sub-operations
committed

April 2024

coqbot-app[bot]
Merge PR #18938: Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed
Gaëtan Gilbert
Add EConstr.ERelevance abstraction barrier to force normalizing relevances
committed

February 2024

coqbot-app[bot]
Merge PR #18639: Fast path for equality function used in the progress tactical.
committed