fixed bug #1780: a lift was missing (match predicate)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11017 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 15 insertions, 2 deletions

diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index 384c4b221..3aa7d7112 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Names
 open Declarations
@@ -220,7 +220,8 @@ and nf_predicate env ind mip params v pT =
       let name = Name (id_of_string "c") in
       let n = mip.mind_nrealargs in
       let rargs = Array.init n (fun i -> mkRel (n-i)) in
-      let dom = mkApp(mkApp(mkInd ind,params),rargs) in
+      let params = if n=0 then params else Array.map (lift n) params in
+      let dom = mkApp(mkInd ind,Array.append params rargs) in
       let body = nf_vtype (push_rel (name,None,dom) env) vb in
       true, mkLambda(name,dom,body)
   | _, _ -> false, nf_val env v crazy_type
diff --git a/test-suite/bugs/closed/1780.v b/test-suite/bugs/closed/1780.v
new file mode 100644
index 000000000..3929fbae2
--- /dev/null
+++ b/test-suite/bugs/closed/1780.v
@@ -0,0 +1,12 @@
+
+Definition bug := Eval vm_compute in eq_rect.
+(* bug:
+Error: Illegal application (Type Error): 
+The term "eq" of type "forall A : Type, A -> A -> Prop"
+cannot be applied to the terms
+ "x" : "A"
+ "P" : "A -> Type"
+ "x0" : "A"
+The 1st term has type "A" which should be coercible to 
+"Type".
+*)