From c08977ff52424b39c92d8bf6aa97255c0a718e50 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 26 Oct 2014 15:20:06 +0100
Subject: Applying like-first selection for destruct in hypotheses.

---
 pretyping/unification.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8b14feca04..1a1d03cc8a 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1481,7 +1481,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
         else
           (push_named_context_val d sign,depdecls)
     | (AtOccs (AllOccurrences, InHyp) | LikeFirst) as occ ->
-        let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
+        let newdecl = replace_term_occ_decl_modulo LikeFirst test mkvarid d in
         if Context.eq_named_declaration d newdecl
            && not (indirectly_dependent c d depdecls)
         then
-- 
cgit v1.2.3