diff options
| author | coq | 2002-10-01 07:53:07 +0000 |
|---|---|---|
| committer | coq | 2002-10-01 07:53:07 +0000 |
| commit | 02f6cb08e4b8f892594934766a40413a3fa30342 (patch) | |
| tree | 6c8e85d78ffbad43aa579ec3612cb93b14f1b4b2 /pretyping/cases.ml | |
| parent | e6afa737d4bcc1c7973cd46094e824b875fede11 (diff) | |
Vraie substitutivite de autohints
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3055 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/cases.ml')
| -rw-r--r-- | pretyping/cases.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index c552be7d6e..4c6e5bb014 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1148,7 +1148,7 @@ let specialize_predicate tomatchs deps cs = function let pred'' = subst_predicate (argsi, copti) pred' in (* We adjust pred st: gamma, x1..xn, x1..xn |- pred'' *) let pred''' = liftn_predicate n (n+1) pred'' in - (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred'''*) + (* We finally get gamma,x1..xn |- [X1,x1:=R1,x1]..[Xn,xn:=Rn,xn]pred''' *) snd (List.fold_right2 (expand_arg n) tomatchs deps (n,pred''')) |