diff options
Diffstat (limited to 'lib')
| -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 |