Commit 93e93a80 authored by Beta Ziliani's avatar Beta Ziliani

kids, never forget to pull before introducing changes (I am the kid, no offence meant to nobody)

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