From 5c30cf26474aa4f52d26005c797130a0d6d21ab5 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 20 May 2017 18:23:05 +0200
Subject: Fixing a failure to interpret some local implicit arguments in
 Inductive.

For instance, the following was failing to use the implicitness of n:

Inductive A (P:forall m {n}, n=m -> Prop) := C : P 0 eq_refl -> A P.
---
 interp/constrintern.ml  | 4 ++--
 interp/constrintern.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287efc..3dfc850410 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -190,10 +190,10 @@ let compute_internalization_data env ty typ impl =
   let expls_impl = compute_explicitable_implicit impl ty in
   (ty, expls_impl, impl, compute_arguments_scope typ)
 
-let compute_internalization_env env ty =
+let compute_internalization_env env ?(impls=empty_internalization_env) ty =
   List.fold_left3
     (fun map id typ impl -> Id.Map.add id (compute_internalization_data env ty typ impl) map)
-    empty_internalization_env
+    impls
 
 (**********************************************************************)
 (* Contracting "{ _ }" in notations *)
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 644cafe575..f3306b5929 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -61,7 +61,7 @@ val empty_internalization_env : internalization_env
 val compute_internalization_data : env -> var_internalization_type ->
   types -> Impargs.manual_explicitation list -> var_internalization_data
 
-val compute_internalization_env : env -> var_internalization_type ->
+val compute_internalization_env : env -> ?impls:internalization_env -> var_internalization_type ->
   Id.t list -> types list -> Impargs.manual_explicitation list list ->
   internalization_env
 
-- 
cgit v1.2.3