From 9e7dc5fd80af6be487813a1ad1a79115b082a343 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 20 Dec 2000 10:56:51 +0000
Subject: Ajout set_lc

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

diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index dabe5cb00f..9097870743 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -38,6 +38,8 @@ let set_pgm pgm ctxt = { ctxt with pgm = pgm }
 
 let get_lc gl = (out_some gl.evar_info).lc
 
+let set_lc lc ctxt = { ctxt with lc = lc }
+
 (* Functions on proof trees *)
 
 let ref_of_proof pf =
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 043e391702..a76eba1cbe 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -22,6 +22,7 @@ val get_ctxt   : goal -> ctxtty
 val get_pgm    : goal -> constr option
 val set_pgm    : constr option -> ctxtty -> ctxtty
 val get_lc     : goal -> local_constraints
+val set_lc     : local_constraints -> ctxtty -> ctxtty
 
 val rule_of_proof     : proof_tree -> rule
 val ref_of_proof      : proof_tree -> (rule * proof_tree list)
-- 
cgit v1.2.3