diff options
Diffstat (limited to 'plugins/subtac/test/wf.v')
| -rw-r--r-- | plugins/subtac/test/wf.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/subtac/test/wf.v b/plugins/subtac/test/wf.v index 49fec2b80..5ccc154af 100644 --- a/plugins/subtac/test/wf.v +++ b/plugins/subtac/test/wf.v @@ -29,7 +29,7 @@ Require Import Wf_nat. Program Fixpoint euclid (a : nat) (b : { b : nat | b <> O }) {wf a lt} : { q : nat & { r : nat | a = b * q + r /\ r < b } } := - if le_lt_dec b a then let (q', r) := euclid (a - b) b in + if le_lt_dec b a then let (q', r) := euclid (a - b) b in (S q' & r) else (O & a). destruct b ; simpl_subtac. |