diff options
Diffstat (limited to 'vernac/proof_using.ml')
| -rw-r--r-- | vernac/proof_using.ml | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index d859fcafe2..01e7b7cc3d 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -64,6 +64,12 @@ let process_expr env sigma e ty = let s = Id.Set.union v_ty (process_expr env sigma e v_ty) in Id.Set.elements s +type t = Names.Id.Set.t + +let definition_using env evd ~using ~terms = + let l = process_expr env evd using terms in + Names.Id.Set.(List.fold_right add l empty) + let name_set id expr = known_names := (id,expr) :: !known_names let minimize_hyps env ids = |