diff options
| author | Brian Campbell | 2019-05-21 12:42:09 +0100 |
|---|---|---|
| committer | Brian Campbell | 2019-05-21 12:42:09 +0100 |
| commit | 6328da7d2ce8e2c1f378c941f25739f60d55570b (patch) | |
| tree | 585cd081e2c1e3e03ac2b115f6ec7aa5a90415f0 /lib/coq | |
| parent | a1166afa11ddd8b6f60e3959b962776413dcb05e (diff) | |
Coq: remove premature unfolding of local definitions
Diffstat (limited to 'lib/coq')
| -rw-r--r-- | lib/coq/Sail2_values.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/lib/coq/Sail2_values.v b/lib/coq/Sail2_values.v index 8323ccfd..61e2c6a4 100644 --- a/lib/coq/Sail2_values.v +++ b/lib/coq/Sail2_values.v @@ -1126,7 +1126,7 @@ Ltac extract_properties := let x := fresh "x" in let Hx := fresh "Hx" in destruct X as [x Hx] in *; - change (projT1 (existT _ x Hx)) with x in *; unfold H in * end; + change (projT1 (existT _ x Hx)) with x in * end; (* Properties in the goal *) repeat match goal with |- context [projT1 ?X] => let x := fresh "x" in |