From 6b691bbd2101fd39395c0d2135fd7c06a8915e14 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 24 Dec 2010 11:53:29 +0100 Subject: Imported Upstream version 8.3pl1 --- pretyping/cases.ml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 09603d8b..bae89329 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: cases.ml 13511 2010-10-06 20:48:16Z herbelin $ *) +(* $Id: cases.ml 13728 2010-12-19 11:35:20Z herbelin $ *) open Util open Names @@ -1648,9 +1648,11 @@ let prepare_predicate loc typing_fun evdref env tomatchs sign tycon pred = let sigma2,pred2 = build_inversion_problem loc env !evdref tomatchs t in [!evdref, KnownDep, pred1; sigma2, DepUnknown, pred2] | None, Some (None, t) -> - (* Only one strategy: we build an "inversion" predicate *) - let sigma,pred = build_inversion_problem loc env !evdref tomatchs t in - [sigma, DepUnknown, pred] + (* First strategy: we build an "inversion" predicate *) + let sigma1,pred = build_inversion_problem loc env !evdref tomatchs t in + (* Second strategy: we abstract the tycon wrt to the dependencies *) + let pred2 = lift (List.length names) t in + [sigma1, DepUnknown, pred; !evdref, KnownNotDep, pred2] | None, _ -> (* No type constaints: we use two strategies *) let t = mkExistential env ~src:(loc, CasesType) evdref in -- cgit v1.2.3