diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-20 08:32:14 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-12-20 08:32:14 +0000 |
| commit | 4a9b25b317e385e26d48979dc40042cd7529959e (patch) | |
| tree | 62c5acd3ea5cdd7670861b8815f977c5c98af420 /pretyping | |
| parent | 3d7219b7796d1baec524141d224ffc3fa79ab3b4 (diff) | |
Non dépliage des Fix non réductibles dans Hnf
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2354 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 2f2f7e753..151525c31 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -547,9 +547,9 @@ let hnf_constr env sigma c = with Redelimination -> match reference_opt_value sigma env ref with | Some c -> - (match kind_of_term c with - | CoFix _ -> app_stack (x,largs) - | _ -> redrec (c, largs)) + (match kind_of_term (snd (decompose_lam c)) with + | CoFix _ | Fix _ -> app_stack (x,largs) + | _ -> redrec (c, largs)) | None -> app_stack s) | _ -> app_stack s in |