diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 19:13:04 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-03-21 19:13:04 +0000 |
| commit | d223f85d0fd57ce74dcdcc8690a36f1ef87b408d (patch) | |
| tree | 4f3fa4d34ae00cb438f5b5d77087d89edeca027f /pretyping/tacred.ml | |
| parent | f687552465f86bfd66ada997a26486b2a20d5363 (diff) | |
Using hnf instead of "intro H" for forcing reduction to a product.
Added full betaiota in hnf. This seems more natural, even if it
changes the strict meaning of hnf. This is source of incompatibilities
as "intro" might succeed more often.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16338 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 86195edd2..508569f0d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -812,7 +812,7 @@ let try_red_product env sigma c = let red_product env sigma c = try try_red_product env sigma c - with Redelimination -> error "Not reducible." + with Redelimination -> error "No head constant to reduce." (* (* This old version of hnf uses betadeltaiota instead of itself (resp @@ -882,8 +882,9 @@ let whd_simpl_orelse_delta_but_fix env sigma c = | CoFix _ | Fix _ -> s' | _ -> redrec (applist(c, stack))) | None -> s' - else s' - in applist (redrec c) + else s' in + let simpfun = clos_norm_flags betaiota env sigma in + simpfun (applist (redrec c)) let hnf_constr = whd_simpl_orelse_delta_but_fix |