From 84c4f0e509dc6cde3a53dda3ba946077cc23ad95 Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack
Date: Fri, 6 Dec 2013 16:45:10 +0100
Subject: Fix test-suite/success/evars.v.

In commit a92a27 (Fix the compilation of pattern matching wrt to variables), I introduced a serious bug in which, in some case, the infered return predicate of a pattern matching would be lifted wrongly. Because I wrote [false] instead of [true] at one location (which prevented creation of aliases and so created shorter named_context than expected).---
 pretyping/cases.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index a5e822862e..b0a4ebea41 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1681,7 +1681,7 @@ let build_inversion_problem loc env sigma tms t =
   let sub_tms =
     List.map2 (fun deps (tm,(tmtyp,_),(na,b,t)) ->
       let na = if List.is_empty deps then Anonymous else force_name na in
-      Pushed (false,((tm,tmtyp),deps,na)))
+      Pushed (true,((tm,tmtyp),deps,na)))
       dep_sign decls in
   let subst = List.map (fun (na,t) -> (na,lift n t)) subst in
   (* [eqn1] is the first clause of the auxiliary pattern-matching that
-- 
cgit v1.2.3