Commit 79196f53 authored by MARCHE Claude's avatar MARCHE Claude

Do not warn on clone instead of use if theory contains an axiom

parent 13c0aa3d
......@@ -717,6 +717,7 @@ let warn_clone_not_abstract loc th =
begin match d.d_node with
| Dtype { ts_def = None }
| Dparam _ -> raise Exit
| Dprop(Paxiom, _,_) -> raise Exit
| _ -> ()
end
| _ -> ()
......
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