diff options
| author | herbelin | 2011-12-18 23:56:06 +0000 |
|---|---|---|
| committer | herbelin | 2011-12-18 23:56:06 +0000 |
| commit | dadfbd96378d4c1b794ffc341bd10cc4d63b225d (patch) | |
| tree | 7ff1c2d295f7ff831302b92de6f00f686d0c9f3b /proofs | |
| parent | 5536b6d56226c4e53bbd6c5ae9a2c419c6f08874 (diff) | |
Granted legitimate wish #2607 (not exposing crude fixpoint body of
unfolded fixpoints when calling destruct). However, this might break
compatibility.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14823 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/logic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index 3801a6fd88..a363c6bbb0 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -451,7 +451,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc',ct,sigma,c') = mk_hdgoals sigma goal goalacc c in let (acc'',pt,sigma,p') = mk_hdgoals sigma goal acc' p in let indspec = - try find_mrectype env sigma ct + try Tacred.find_hnf_rectype env sigma ct with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = type_case_branches_with_names env indspec p c in |