Skip to content

Commit

Permalink
Don't complain about reregistering a hook afte backtracking
Browse files Browse the repository at this point in the history
When doing the following since coq#17794

```Coq
Declare ML Module "module-declaring-a-coercion-hook".
(* <backtrack> *)
(* <reexecute previous command> *)
```

Coq complained about "Hook already registered". To avoid that,
this commit puts the set of registered hooks under a summary.
  • Loading branch information
proux01 committed Jul 17, 2023
1 parent 6b4794c commit 9e22dd5
Showing 1 changed file with 5 additions and 2 deletions.
7 changes: 5 additions & 2 deletions pretyping/coercion.ml
Expand Up @@ -627,13 +627,16 @@ type hook = env -> evar_map -> flags:Evarconv.unify_flags -> constr ->

let all_hooks = ref (CString.Map.empty : hook CString.Map.t)

let registered_hooks = Summary.ref ~name:"coercion_hooks" CString.Set.empty

let register_hook ~name ?(override=false) h =
if not override && CString.Map.mem name !all_hooks then
if not override && CString.Set.mem name !registered_hooks then
CErrors.anomaly ~label:"Coercion.register_hook"
Pp.(str "Hook already registered: \"" ++ str name ++ str "\".");
registered_hooks := CString.Set.add name !registered_hooks;
all_hooks := CString.Map.add name h !all_hooks

let active_hooks = Summary.ref ~name:"coercion_hooks" ([] : string list)
let active_hooks = Summary.ref ~name:"coercion_hooks_active" ([] : string list)

let deactivate_hook ~name =
active_hooks := List.filter (fun s -> not (String.equal s name)) !active_hooks
Expand Down

0 comments on commit 9e22dd5

Please sign in to comment.