diff options
Diffstat (limited to 'src/NewBaseSystem.v')
| -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; |