From a45bd5981092cceefc4d4d30f9be327bb69c22d8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Tue, 21 Apr 2015 16:36:31 +0200
Subject: Fixing #4198 (looking for subterms also in the return clause of
 match).

This is actually not so perfect because of the lambdas in the return
clause which we would not like to look in.
---
 dev/base_include             | 1 +
 pretyping/constr_matching.ml | 2 +-
 2 files changed, 2 insertions(+), 1 deletion(-)

diff --git a/dev/base_include b/dev/base_include
index de63c557d3..d58b6ad13c 100644
--- a/dev/base_include
+++ b/dev/base_include
@@ -86,6 +86,7 @@ open Cbv
 open Classops
 open Clenv
 open Clenvtac
+open Constr_matching
 open Glob_term
 open Glob_ops
 open Coercion
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 161cffa865..e281807131 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -428,7 +428,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
       | [] -> assert false
       | c1 :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
       in
-      let sub = (env, c1) :: subargs env lc in
+      let sub = (env, hd) :: (env, c1) :: subargs env lc in
       let next () = try_aux sub next_mk_ctx next in
       authorized_occ env sigma partial_app closed pat c mk_ctx next
   | Fix (indx,(names,types,bodies)) ->
-- 
cgit v1.2.3