From 677e4ba54813f873c4e0e347cf88357b94c627e8 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 3 Dec 1999 14:24:22 +0000
Subject:  - coqmktop  - #use "include.ml";;

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@198 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenv.ml  | 19 +++++++++++++++++++
 proofs/clenv.mli |  3 +++
 2 files changed, 22 insertions(+)

(limited to 'proofs')

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 5f6af5a8b3..0131df8b94 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -1050,3 +1050,22 @@ let elim_res_pf kONT clenv gls =
 let e_res_pf kONT clenv gls =
   clenv_refine kONT
     (clenv_pose_dependent_evars (clenv_unique_resolver false clenv gls)) gls
+
+open Printer
+
+let pr_clenv clenv =
+  let pr_name mv =
+    try 
+      let id = Intmap.find mv clenv.namenv in
+      [< 'sTR"[" ; print_id id ; 'sTR"]" >]
+    with Not_found -> [< >]
+  in
+  let pr_meta_binding = function
+    | (mv,Cltyp b) ->
+      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " : " ; prterm b.rebus ; 'fNL >]
+    | (mv,Clval(b,_)) ->
+      	hOV 0 [< 'iNT mv ; pr_name mv ; 'sTR " := " ; prterm b.rebus ; 'fNL >]
+  in
+  [< 'sTR"TEMPL: " ; prterm clenv.templval.rebus ;
+     'sTR" : " ; prterm clenv.templtyp.rebus ; 'fNL ;
+     (prlist pr_meta_binding (intmap_to_list clenv.env)) >]
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index f5daf8b361..1f28a73afe 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -92,3 +92,6 @@ val clenv_constrain_dep_args_of :
 val constrain_clenv_using_subterm_list : 
   bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
 val clenv_typed_unify : constr -> constr -> wc clausenv -> wc clausenv
+
+val pr_clenv : 'a clausenv -> Pp.std_ppcmds
+
-- 
cgit v1.2.3