diff options
| author | msozeau | 2010-06-08 01:04:50 +0000 |
|---|---|---|
| committer | msozeau | 2010-06-08 01:04:50 +0000 |
| commit | 9ff883b56b53944e28a495fe17dfa467382b645c (patch) | |
| tree | 2d216a9d87234ae04d7ee52c6d89539d9bbd9a77 | |
| parent | a9dc8d481853386e620ff50f345b361b4902d32c (diff) | |
Fix unfolding tactic for well-founded Programs.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13088 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | theories/Program/Wf.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 70a6fe97a4..7179135726 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -213,7 +213,7 @@ Ltac fold_sub f := match goal with | [ |- ?T ] => match T with - appcontext C [ @Fix_sub _ _ _ _ ?arg ] => + appcontext C [ @Fix_sub _ _ _ _ _ ?arg ] => let app := context C [ f arg ] in change app end @@ -250,6 +250,6 @@ Module WfExtensionality. Ltac unfold_sub f fargs := set (call:=fargs) ; unfold f in call ; unfold call ; clear call ; - rewrite fix_sub_eq_ext ; repeat fold_sub fargs ; simpl proj1_sig. + rewrite fix_sub_eq_ext ; repeat fold_sub f ; simpl proj1_sig. End WfExtensionality. |