From 45804f0dc095b044b7a5bf4bdb86fd42045e7ee3 Mon Sep 17 00:00:00 2001
From: corbinea
Date: Mon, 29 Jan 2007 17:14:50 +0000
Subject: bugfix for suffices (support for open head)

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

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 0a984cceb9..f341580eb1 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -204,7 +204,7 @@ let rawconstr_of_hyps inject hyps head =
 let raw_prop = RSort (dummy_loc,RProp Null)
   
 let rec match_hyps blend names constr = function 
-    [] -> [],constr
+    [] -> [],substl names constr
   | hyp::q -> 
       let (name,typ,body)=destProd constr in
       let st= {st_label=name;st_it=substl names typ} in
-- 
cgit v1.2.3