diff options
Diffstat (limited to 'proofs/logic.ml')
| -rw-r--r-- | proofs/logic.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml index caf6f56b..c019d45f 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: logic.ml 12168 2009-06-06 21:34:37Z herbelin $ *) +(* $Id: logic.ml 12240 2009-07-15 09:52:52Z herbelin $ *) open Pp open Util @@ -438,7 +438,7 @@ and mk_casegoals sigma goal goalacc p c = let (acc'',pt) = mk_hdgoals sigma goal acc' p in let pj = {uj_val=p; uj_type=pt} in let indspec = - try find_mrectype env sigma ct + try find_mrectype env sigma (nf_evar sigma ct) with Not_found -> anomaly "mk_casegoals" in let (lbrty,conclty) = type_case_branches_with_names env indspec pj c in |