diff options
| author |  jadep <jade.philipoom@gmail.com> | 2017-03-06 14:36:47 -0500 |
|---|---|---|
| committer | jadep <jade.philipoom@gmail.com> | 2017-03-06 14:36:51 -0500 |
| commit | 04f2699445877ee8e0b9616ce2ad7ccd57889593 (patch) | |
| tree | 6d510295dc2fdfc77476af64e131edbd4ae58dff | |
| parent | efb6df34a759e954108796cdc7f4dbbab5038e74 (diff) | |
Fixes #127
| -rw-r--r-- | src/NewBaseSystem.v | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/NewBaseSystem.v b/src/NewBaseSystem.v index dbd06671c..70c44fd48 100644 --- a/src/NewBaseSystem.v +++ b/src/NewBaseSystem.v @@ -874,8 +874,7 @@ Ltac F_mod_eq := Ltac solve_op_mod_eq wt x := transitivity (Positional.eval wt x); autounfold; - [|assert_preconditions; - autorewrite with uncps push_id push_basesystem_eval; + [|autorewrite with uncps push_id push_basesystem_eval; reflexivity]; cbv [mod_eq]; apply f_equal2; [|reflexivity]; apply f_equal; |