Commit ae62fcce authored by Guillaume Melquiond's avatar Guillaume Melquiond

Prevent anomaly on accessing the missing body of opaque constants in the Coq tactic.

parent 90958d5d
......@@ -73,7 +73,10 @@ let declare_summary name freeze unfreeze init =
let body_of_constant env c =
if Reductionops.is_transparent env (ConstKey c) then
Declareops.body_of_constant Opaqueproof.empty_opaquetab (Global.lookup_constant c)
let cb = Environ.lookup_constant c env in
match cb.const_body with
| Def _ -> Declareops.body_of_constant Opaqueproof.empty_opaquetab cb
| _ -> None
else None
let get_transp_state env =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment