From f34625ec7bbd0b2b6e2ce02a978d089b47c152ba Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Sep 2010 20:21:02 +0000
Subject: Fixing bug #2360 (descend_in_conjunctions built ill-typed terms).
 Shouldn't we revert the catch of anomalies in reductionops.ml now (commit
 13353)?

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13439 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b253b2375e..b9cea418d8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -884,7 +884,8 @@ let make_projection params cstr sign elim i n c =
       match List.nth l i with
       | Some proj ->
 	  let t = Typeops.type_of_constant (Global.env()) proj in
-	  Some (beta_applist (mkConst proj,params),prod_applist t (params@[c]))
+	  let args = extended_rel_vect 0 sign in
+	  Some (beta_applist (mkConst proj,params),prod_applist t (params@[mkApp (c,args)]))
       | None -> None
   in Option.map (fun (abselim,elimt) -> 
     let c = beta_applist (abselim,[mkApp (c,extended_rel_vect 0 sign)]) in
-- 
cgit v1.2.3