From cde6f21cd5cf45303f597bcda5b4a377ef93e74a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 29 Mar 2003 14:33:17 +0000
Subject: Implicit Variables Type dans les inductive

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3808 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml  | 4 ++++
 interp/constrintern.mli | 1 +
 2 files changed, 5 insertions(+)

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 9ab3ddf42f..b476320150 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -590,6 +590,10 @@ let interp_casted_openconstr sigma env c typ =
 let interp_type sigma env c =
   understand_type sigma env (interp_rawtype sigma env c)
 
+let interp_binder sigma env na t =
+  let t = interp_rawtype sigma env t in
+  understand_type sigma env (locate_if_isevar (loc_of_rawconstr t) na t)
+
 let interp_type_with_implicits sigma env impls c =
   understand_type sigma env (interp_rawtype_with_implicits sigma env impls c)
 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 5478957b56..5d66424c24 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -49,6 +49,7 @@ val interp_rawconstr_gen : bool -> evar_map -> env -> implicits_env ->
 val interp_constr        : evar_map -> env -> constr_expr -> constr
 val interp_casted_constr : evar_map -> env -> constr_expr -> types -> constr
 val interp_type          : evar_map -> env -> constr_expr -> types
+val interp_binder          : evar_map -> env -> name -> constr_expr -> types
 val interp_openconstr    : evar_map -> env -> constr_expr -> evar_map * constr
 val interp_casted_openconstr    :
   evar_map -> env -> constr_expr -> constr -> evar_map * constr
-- 
cgit v1.2.3