diff options
Diffstat (limited to 'toplevel/backtrack.ml')
| -rw-r--r-- | toplevel/backtrack.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/backtrack.ml b/toplevel/backtrack.ml index 37496387e..2d1e1c6a3 100644 --- a/toplevel/backtrack.ml +++ b/toplevel/backtrack.ml @@ -32,7 +32,7 @@ open Vernacexpr type info = { label : int; nproofs : int; - prfname : identifier option; + prfname : Id.t option; prfdepth : int; ngoals : int; cmd : vernac_expr; @@ -228,7 +228,7 @@ let get_script prf = let script = ref [] in let select i = match i.prfname with | None -> raise Not_found - | Some p when id_eq p prf && i.reachable -> script := i :: !script + | Some p when Id.equal p prf && i.reachable -> script := i :: !script | _ -> () in (try Stack.iter select history with Not_found -> ()); |