From 40ea8e13306f2eed48a7b6894c3d9b8822ac9b53 Mon Sep 17 00:00:00 2001
From: bertot
Date: Tue, 21 Jan 2003 10:18:06 +0000
Subject: Make sure pcoq will also display hypotheses with a value.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3553 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/interface/translate.ml | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

(limited to 'contrib/interface')

diff --git a/contrib/interface/translate.ml b/contrib/interface/translate.ml
index 96049aed60..e63baecfb5 100644
--- a/contrib/interface/translate.ml
+++ b/contrib/interface/translate.ml
@@ -114,9 +114,16 @@ let translate_constr at_top env c =
 (* this code is inspired from printer.ml (function pr_named_context_of) *)
 let translate_sign env =
   let l = 
-    fold_named_context
+    Environ.fold_named_context
       (fun env (id,v,c) l -> 
-	 (CT_premise(CT_ident(string_of_id id), translate_constr false env c))::l)
+	 (match v with
+	      None ->
+	       	CT_premise(CT_ident(string_of_id id), translate_constr false env c)
+	    | Some v1 ->
+		CT_eval_result
+		  (CT_coerce_ID_to_FORMULA (CT_ident (string_of_id id)),
+		   translate_constr false env v1,
+		   translate_constr false env c))::l)
       env ~init:[] 
   in
   CT_premises_list l;;
-- 
cgit v1.2.3