diff options
| author | barras | 2004-09-07 19:28:25 +0000 |
|---|---|---|
| committer | barras | 2004-09-07 19:28:25 +0000 |
| commit | d331f7f1ac0ec2ed12d458597d558a1988db1ba6 (patch) | |
| tree | 0e5addad213aeb1d647a0411285754e8a9cb23f6 /contrib/xml/proofTree2Xml.ml4 | |
| parent | 11104cdcb1e53cd83768d2ce9858829b457e2d65 (diff) | |
deuxieme vague de modifs: evar_defs fonctionnel
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/xml/proofTree2Xml.ml4')
| -rw-r--r-- | contrib/xml/proofTree2Xml.ml4 | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/contrib/xml/proofTree2Xml.ml4 b/contrib/xml/proofTree2Xml.ml4 index b9b66774a5..4239917845 100644 --- a/contrib/xml/proofTree2Xml.ml4 +++ b/contrib/xml/proofTree2Xml.ml4 @@ -95,7 +95,7 @@ let string_of_prim_rule x = match x with let - print_proof_tree curi sigma0 pf proof_tree_to_constr + print_proof_tree curi sigma pf proof_tree_to_constr proof_tree_to_flattened_proof_tree constr_to_ids = let module PT = Proof_type in @@ -164,10 +164,7 @@ Pp.ppnl (Pp.(++) (Pp.str let {Evd.evar_concl=concl; Evd.evar_hyps=hyps}=goal in - let rc = (Proof_trees.rc_of_gc sigma0 goal) in - let sigma = Proof_trees.get_gc rc in - let hyps = Proof_trees.get_hyps rc in - let env= Proof_trees.get_env rc in + let env = Global.env_of_context hyps in let xgoal = X.xml_nempty "Goal" [] (constr_to_xml concl sigma env) in |