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 /tactics | |
| 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 'tactics')
| -rw-r--r-- | tactics/tactics.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 59e023762..ac783adf3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -443,9 +443,9 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl = (* that intro do betaiotazeta only when reduction is needed; and *) (* probably also a pity that intro does zeta *) try - tclTHEN try_red_in_concl - (intro_then_gen loc name_flag move_flag force_flag dep_flag tac) gl - with Redelimination -> + tclTHEN hnf_in_concl + (intro_then_gen loc name_flag move_flag false dep_flag tac) gl + with RefinerError IntroNeedsProduct -> user_err_loc(loc,"Intro",str "No product even after head-reduction.") let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> tclIDTAC) |