diff options
| author |  Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2010-12-24 11:53:29 +0100 |
| commit | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (patch) | |
| tree | b04b45d1a6f42d19b1428c522d647afbad2f9b83 /pretyping | |
| parent | 3e96002677226c0cdaa8f355938a76cfb37a722a (diff) | |
Imported Upstream version 8.3pl1upstream/8.3pl1
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 10 |
1 files changed, 6 insertions, 4 deletions
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 |