Commit 4145fe5b authored by Janno's avatar Janno

Revert "Make heap_lang/tactics.v universe polymorphic."

This reverts commit 8c9b610e.
parent 8c9b610e
......@@ -6,10 +6,6 @@ Delimit Scope typed_tactic_scope with TT.
Set Default Proof Using "Type".
Import heap_lang.
Set Universe Polymorphism.
Set Polymorphic Inductive Cumulativity.
Unset Universe Minimization ToSet.
(** We define an alternative representation of expressions in which the
embedding of values and closed expressions is explicit. By reification of
expressions into this type we can implementation substitution, closedness
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