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

1 files changed, 4 insertions, 1 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 869497764..46dabb266 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