From 908223f97c27ed33ddd867dfb12a63b294b399ad Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 30 Jun 2007 11:01:05 +0000
Subject: Factorisation des types dans l'affichage des paramètres des
 (Co)Inductif/Record

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

(limited to 'interp')

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index cf4d2db0e4..37e47301ac 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -992,3 +992,8 @@ and raw_of_eqn env constr construct_nargs branch =
 
 let extern_constr_pattern env pat =
   extern true (None,[]) Idset.empty (raw_of_pat env pat)
+
+let extern_rel_context where env sign =
+  let a = detype_rel_context where [] (names_of_rel_context env) sign in
+  let vars = vars_of_env env in
+  snd (extern_local_binder (None,[]) vars a)
diff --git a/interp/constrextern.mli b/interp/constrextern.mli
index a0f8661ccd..7ae2977f5c 100644
--- a/interp/constrextern.mli
+++ b/interp/constrextern.mli
@@ -42,6 +42,8 @@ val extern_constr_in_scope : bool -> scope_name -> env -> constr -> constr_expr
 val extern_reference : loc -> Idset.t -> global_reference -> reference
 val extern_type : bool -> env -> types -> constr_expr
 val extern_sort : sorts -> rawsort
+val extern_rel_context : constr option -> env -> 
+  rel_context -> local_binder list
 
 (* Printing options *)
 val print_implicits : bool ref
-- 
cgit v1.2.3