diff options
| -rw-r--r-- | doc/sphinx/proof-engine/proof-handling.rst | 4 | ||||
| -rw-r--r-- | test-suite/bugs/closed/bug_12930.v | 10 | ||||
| -rw-r--r-- | vernac/proof_using.ml | 23 |
3 files changed, 25 insertions, 12 deletions
diff --git a/doc/sphinx/proof-engine/proof-handling.rst b/doc/sphinx/proof-engine/proof-handling.rst index 4480b10319..55e4f26fe8 100644 --- a/doc/sphinx/proof-engine/proof-handling.rst +++ b/doc/sphinx/proof-engine/proof-handling.rst @@ -156,6 +156,10 @@ list of assertion commands is given in :ref:`Assertions`. The command ``T``, then the commands ``Proof using a`` and ``Proof using T a`` are equivalent. + The set of declared variables always includes the variables used by + the statement. In other words ``Proof using e`` is equivalent to + ``Proof using Type + e`` for any declaration expression ``e``. + .. cmdv:: Proof using {+ @ident } with @tactic Combines in a single line :cmd:`Proof with` and :cmd:`Proof using`. diff --git a/test-suite/bugs/closed/bug_12930.v b/test-suite/bugs/closed/bug_12930.v new file mode 100644 index 0000000000..e2a524301a --- /dev/null +++ b/test-suite/bugs/closed/bug_12930.v @@ -0,0 +1,10 @@ +Section S. + Variable v : Prop. + Variable vv : v. + Collection easy := Type*. + + Lemma ybar : v. + Proof using easy. + exact vv. + Qed. +End S. diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml index 2130a398e9..95680c2a4e 100644 --- a/vernac/proof_using.ml +++ b/vernac/proof_using.ml @@ -41,28 +41,27 @@ let set_of_type env ty = let full_set env = List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty -let rec process_expr env e ty = +let process_expr env e v_ty = let rec aux = function | SsEmpty -> Id.Set.empty - | SsType -> set_of_type env ty - | SsSingl { CAst.v = id } -> set_of_id env id + | SsType -> v_ty + | SsSingl { CAst.v = id } -> set_of_id id | SsUnion(e1,e2) -> Id.Set.union (aux e1) (aux e2) | SsSubstr(e1,e2) -> Id.Set.diff (aux e1) (aux e2) | SsCompl e -> Id.Set.diff (full_set env) (aux e) | SsFwdClose e -> close_fwd env (aux e) + and set_of_id id = + if Id.to_string id = "All" then + full_set env + else if CList.mem_assoc_f Id.equal id !known_names then + aux (CList.assoc_f Id.equal id !known_names) + else Id.Set.singleton id in - aux e - -and set_of_id env id = - if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty - else if CList.mem_assoc_f Id.equal id !known_names then - process_expr env (CList.assoc_f Id.equal id !known_names) [] - else Id.Set.singleton id + aux e let process_expr env e ty = let v_ty = set_of_type env ty in - let s = Id.Set.union v_ty (process_expr env e ty) in + let s = Id.Set.union v_ty (process_expr env e v_ty) in Id.Set.elements s let name_set id expr = known_names := (id,expr) :: !known_names |