From 04f2699445877ee8e0b9616ce2ad7ccd57889593 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 6 Mar 2017 14:36:47 -0500 Subject: Fixes #127 --- src/NewBaseSystem.v | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'src/NewBaseSystem.v') 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; -- cgit v1.2.3