From 166714d89845f7e2f894fcd0fd92ae16961ca9eb Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 25 Apr 2008 11:42:32 +0000
Subject: - Fix bug in eterm which was not taking filtered contexts in evars
 into   account. - Add test case for bug #1844 on Combined Scheme. - Change
 Reflexive_partial_app_morphism to require a Reflexive proof to   cut down
 search earlier, without losing anything.

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

(limited to 'contrib')

diff --git a/contrib/subtac/eterm.ml b/contrib/subtac/eterm.ml
index 9cb65f76e0..8f319f9efc 100644
--- a/contrib/subtac/eterm.ml
+++ b/contrib/subtac/eterm.ml
@@ -141,7 +141,7 @@ let eterm_obligations env name isevars evm fs t ty =
     (* Remove existential variables in types and build the corresponding products *)
     fold_right 
       (fun (id, (n, nstr), ev) l ->
-	 let hyps = Environ.named_context_of_val ev.evar_hyps in
+	 let hyps = Evd.evar_filtered_context ev in
 	 let hyps = trunc_named_context nc_len hyps in
 	 let evtyp, deps, transp = etype_of_evar l hyps ev.evar_concl in
 	 let evtyp, hyps, chop = 
-- 
cgit v1.2.3