diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 01f883cde1..2396db868b 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -207,7 +207,7 @@ let discard (loc,id) = let n = List.length !pstates in discard_gen id; if Int.equal (List.length !pstates) n then - CErrors.user_err ~loc + CErrors.user_err ?loc ~hdr:"Pfedit.delete_proof" (str"No such proof" ++ msg_proofs ()) let discard_current () = @@ -287,13 +287,13 @@ let set_used_variables l = match entry with | LocalAssum (x,_) -> if Id.Set.mem x all_safe then orig - else (ctx, all_safe, (Loc.ghost,x)::to_clear) + else (ctx, all_safe, (Loc.tag x)::to_clear) | LocalDef (x,bo, ty) as decl -> if Id.Set.mem x all_safe then orig else let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in if Id.Set.subset vars all_safe then (decl :: ctx, Id.Set.add x all_safe, to_clear) - else (ctx, all_safe, (Loc.ghost,x) :: to_clear) in + else (ctx, all_safe, (Loc.tag x) :: to_clear) in let ctx, _, to_clear = Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in let to_clear = if !proof_using_auto_clear then to_clear else [] in |