Commit 7f8cc205 authored by Léon Gondelman 's avatar Léon Gondelman

comment out closedness conditions

parent c54446ca
......@@ -184,7 +184,7 @@ Inductive dexpr : Type :=
| dEPair : dexpr dexpr dexpr
| dEFst : dexpr dexpr
| dESnd : dexpr dexpr
| dEUnknown (e : expr) `{!Closed [] e} : dexpr.
| dEUnknown (e : expr) (*`{!Closed [] e}*) : dexpr.
Fixpoint dexpr_interp (E: known_locs) (de: dexpr) : expr :=
match de with
......@@ -209,7 +209,7 @@ Inductive dcexpr : Type :=
| dCSeq : dcexpr dcexpr dcexpr
| dCPar : dcexpr dcexpr dcexpr
| dCInvoke (f: val) (de: dcexpr)
| dCUnknown (e : expr) `{!Closed [] e}.
| dCUnknown (e : expr) (* `{!Closed [] e} *).
Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
match de with
......@@ -485,7 +485,7 @@ Global Instance into_dexpr_snd E e de:
IntoDExpr E (Snd e) (dESnd de).
Proof. intros [-> ?]; split; auto. Qed.
Global Instance into_dexpr_unknown E e `{Closed [] e}:
Global Instance into_dexpr_unknown E e (* `{Closed [] e} *):
IntoDExpr E e (dEUnknown e) | 100.
Proof. done. Qed.
......@@ -559,6 +559,6 @@ Proof.
split; simpl; auto; f_equal; apply HC.
Qed.
Global Instance into_dcexpr_unknown E e `{Closed [] e}:
Global Instance into_dcexpr_unknown E e (* `{Closed [] e} *):
IntoDCExpr E e (dCUnknown e) | 100.
Proof. done. Qed.
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