diff options
| author | filliatr | 1999-12-03 14:24:22 +0000 |
|---|---|---|
| committer | filliatr | 1999-12-03 14:24:22 +0000 |
| commit | 677e4ba54813f873c4e0e347cf88357b94c627e8 (patch) | |
| tree | 8ebfbce51321a78331ee11424b4c8401a5fa4fe9 /proofs | |
| parent | a2dcfb5c3931d1a0f6ee6dce6bedd0c19e439e95 (diff) | |
- coqmktop
- #use "include.ml";;
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@198 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 19 | ||||
| -rw-r--r-- | proofs/clenv.mli | 3 |
2 files changed, 22 insertions, 0 deletions
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 + |