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 +
 1 file changed, 1 insertion(+)

(limited to 'dev')

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
-- 
cgit v1.2.3