From 4e4fb7bd42364fd623f8e0e0d3007cd79d78764b Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 2 Feb 2017 18:21:51 +0100
Subject: Renaming local_binder into local_binder_expr.

This is a bit long, but it is to keep a symmetry with constr_expr.
---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8d5b1e7828..de2fabb9e3 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -813,7 +813,7 @@ let rec chop_n_arrow n t =
       | _ -> anomaly (Pp.str "Not enough products")
 
 
-let rec get_args b t : Constrexpr.local_binder list *
+let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
   match b with
     | Constrexpr.CLambdaN (loc, (nal_ta), b') ->
-- 
cgit v1.2.3