normalize S to (+1) in fsimpl

coq-community · Jan 14, 2016 · 3b5eb02 · 3b5eb02
1 parent 4f8dc59
commit 3b5eb02
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/theories/Autosubst_Basics.v b/theories/Autosubst_Basics.v
@@ -269,6 +269,7 @@ Ltac fsimpl :=
         change ((f >>> g) >>> h) with (f >>> (g >>> h))
     | [|- context[(+0)]] => change (+0) with (@id var)
     | [|- context[0 + ?m]] => change (0 + m) with m
+    | [|- appcontext[?s S]] => change (s S) with (s (+1))
     | [|- context[S ?n + ?m]] => change (S n + m) with (S (n + m))
     | [|- context[(+S ?n) >>> (?x .: ?xr)]] =>
         change ((+S n) >>> (x .: xr)) with ((+n) >>> xr)
@@ -286,6 +287,7 @@ Ltac fsimplH H :=
         change ((f >>> g) >>> h) with (f >>> (g >>> h)) in H
     | context[(+0)] => change (+0) with (@id var) in H
     | context[0 + ?m] => change (0 + m) with m in H
+    | appcontext[?s S] => change (s S) with (s (+1)) in H
     | context[S ?n + ?m] => change (S n + m) with (S (n + m)) in H
     | context[(+S ?n) >>> (?x .: ?xr)] =>
         change ((+S n) >>> (x .: xr)) with ((+n) >>> xr) in H