diff options
| author | herbelin | 2003-10-10 18:53:44 +0000 |
|---|---|---|
| committer | herbelin | 2003-10-10 18:53:44 +0000 |
| commit | 756638978b274a454258991c001c3001d351ff52 (patch) | |
| tree | c135562f126d3c003c8f3f79ce67e2598760073a | |
| parent | 80ec30c8ee117631ff5422bb158e38d847935258 (diff) | |
pf_get_new_id en provenance de feu wcclausenv
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4573 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | proofs/tacmach.ml | 9 | ||||
| -rw-r--r-- | proofs/tacmach.mli | 3 |
2 files changed, 12 insertions, 0 deletions
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index 3de476b172..c7bc2a1d0b 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -66,6 +66,15 @@ let pf_get_hyp_typ gls id = let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls) +let pf_get_new_id id gls = + next_ident_away id (pf_ids_of_hyps gls) + +let pf_get_new_ids ids gls = + let avoid = pf_ids_of_hyps gls in + List.fold_right + (fun id acc -> (next_ident_away id (acc@avoid))::acc) + ids [] + let pf_interp_constr gls c = let evc = project gls in Constrintern.interp_constr evc (pf_env gls) c diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli index 73916c6bbd..931f988dd4 100644 --- a/proofs/tacmach.mli +++ b/proofs/tacmach.mli @@ -60,6 +60,9 @@ val pf_interp_type : goal sigma -> Topconstr.constr_expr -> types val pf_get_hyp : goal sigma -> identifier -> named_declaration val pf_get_hyp_typ : goal sigma -> identifier -> types +val pf_get_new_id : identifier -> goal sigma -> identifier +val pf_get_new_ids : identifier list -> goal sigma -> identifier list + val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr |