Commit 07032585 authored by Maxime Dénès's avatar Maxime Dénès Committed by Guillaume Melquiond

Fix build with Coq 8.7.0.

parent 15cd0092
......@@ -106,8 +106,6 @@ DECLARE PLUGIN "why3tac"
IFDEF COQ87 THEN
let is_Set evd t = is_Set (to_constr evd t)
let is_Type evd t = is_Type (to_constr evd t)
let global_of_constr evd t = global_of_constr (to_constr evd t)
let type_of_global env c = of_constr (fst (Global.type_of_global_in_context env c))
......
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