From 8cd666c100ae757b70d73f502878e4c939864ecc Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 21 Nov 2011 11:41:29 +0000
Subject: Add matching on non-inductive types in building an inversion problem
 for finding the initial predicate, since their type can be dependent on
 previous terms to match and they may have to be generalized.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14710 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/cases.ml | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8694977649..46dabb2662 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1528,7 +1528,10 @@ let build_inversion_problem loc env sigma tms t =
 	let patl',acc_sign,acc = aux (n+p+1) env' (sign@acc_sign) tms acc in
 	patl@pat::patl',acc_sign,acc
     | (t, NotInd (bo,typ)) :: tms ->
-	aux n env acc_sign tms acc in
+      let pat,acc = make_patvar t acc in
+      let d = (alias_of_pat pat,None,t) in
+      let patl,acc_sign,acc = aux (n+1) (push_rel d env) (d::acc_sign) tms acc in
+      pat::patl,acc_sign,acc in
   let avoid0 = ids_of_context env in
   (* [patl] is a list of patterns revealing the substructure of
      constructors present in the constraints on the type of the
-- 
cgit v1.2.3