Commit 8c9b610e authored by Janno's avatar Janno

Make heap_lang/tactics.v universe polymorphic.

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