From bfba94a477393f87a9af8b3e37d15a776ffa4648 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 28 Mar 2007 15:35:41 +0000
Subject: Support for implicit formal argument types in Program ; parse types
 in type scope.

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

(limited to 'interp')

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5a41f35086..f067eda6b5 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1087,6 +1087,8 @@ let intern_gen isarity sigma env
 
 let intern_constr sigma env c = intern_gen false sigma env c 
 
+let intern_type sigma env c = intern_gen true sigma env c 
+
 let intern_pattern env patt =
   try
     intern_cases_pattern env [] ([],[]) None patt 
diff --git a/interp/constrintern.mli b/interp/constrintern.mli
index 1af6854d3e..edbf9fb62a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -51,6 +51,8 @@ type ltac_sign = identifier list * unbound_ltac_var_map
 
 val intern_constr : evar_map -> env -> constr_expr -> rawconstr
 
+val intern_type : evar_map -> env -> constr_expr -> rawconstr
+
 val intern_gen : bool -> evar_map -> env ->
   ?impls:full_implicits_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign ->
   constr_expr -> rawconstr
-- 
cgit v1.2.3