diff options
author | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-08 01:04:50 +0000 |
---|---|---|
committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-08 01:04:50 +0000 |
commit | 9ff883b56b53944e28a495fe17dfa467382b645c (patch) | |
tree | 2d216a9d87234ae04d7ee52c6d89539d9bbd9a77 /theories/Program | |
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
Diffstat (limited to 'theories/Program')
-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 70a6fe97a..717913572 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. |