diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-07-01 17:21:14 +0200 |
| commit | da178a880e3ace820b41d38b191d3785b82991f5 (patch) | |
| tree | 6356ab3164a5ad629f4161dc6c44ead74edc2937 /proofs/logic.ml | |
| parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) | |
Imported Upstream version 8.2pl2+dfsgupstream/8.2.pl2+dfsg
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 |