Commit 7447d217 authored by Janno's avatar Janno

Make proofmode/tactics.v polymorphic.

parent c5ffd28c
......@@ -11,6 +11,10 @@ Delimit Scope typed_tactic_scope with TT.
Set Default Proof Using "Type".
Export ident.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.
Notation env_Reduction := (
RedStrong [rl:RedBeta; RedMatch; RedFix; RedZeta;
RedDeltaOnly
......
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