aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-09-27 16:54:41 +0200
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2017-10-10 23:50:25 +0200
commit74826c1869a423b4e7224d3f69180584bdef1726 (patch)
tree961375ac1a3e386271eaa2b33a49349f38e12fed /vernac
parenta627891e0505e7da7afcb56c79d2058ebf058694 (diff)
Parse [Proof using Type] without translating Type to an id.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/proof_using.ml36
-rw-r--r--vernac/proof_using.mli2
2 files changed, 13 insertions, 25 deletions
diff --git a/vernac/proof_using.ml b/vernac/proof_using.ml
index ade132ae1..ffe99cfd8 100644
--- a/vernac/proof_using.ml
+++ b/vernac/proof_using.ml
@@ -14,16 +14,6 @@ open Context.Named.Declaration
module NamedDecl = Context.Named.Declaration
-let to_string e =
- let rec aux = function
- | SsEmpty -> "()"
- | SsSingl (_,id) -> "("^Id.to_string id^")"
- | SsCompl e -> "-" ^ aux e^""
- | SsUnion(e1,e2) -> "("^aux e1 ^" + "^ aux e2^")"
- | SsSubstr(e1,e2) -> "("^aux e1 ^" - "^ aux e2^")"
- | SsFwdClose e -> "("^aux e^")*"
- in aux e
-
let known_names = Summary.ref [] ~name:"proofusing-nameset"
let in_nameset =
@@ -48,12 +38,20 @@ let rec close_fwd e s =
s (named_context e)
in
if Id.Set.equal s s' then s else close_fwd e s'
-;;
+
+let set_of_type env ty =
+ List.fold_left (fun acc ty ->
+ Id.Set.union (global_vars_set env ty) acc)
+ Id.Set.empty 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 rec aux = function
| SsEmpty -> Id.Set.empty
- | SsSingl (_,id) -> set_of_id env ty id
+ | SsType -> set_of_type env ty
+ | SsSingl (_,id) -> set_of_id env 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)
@@ -61,23 +59,15 @@ let rec process_expr env e ty =
in
aux e
-and set_of_id env ty id =
- if Id.to_string id = "Type" then
- List.fold_left (fun acc ty ->
- Id.Set.union (global_vars_set env ty) acc)
- Id.Set.empty ty
- else if Id.to_string id = "All" then
+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
-and full_set env =
- List.fold_right Id.Set.add (List.map NamedDecl.get_id (named_context env)) Id.Set.empty
-
let process_expr env e ty =
- let ty_expr = SsSingl(Loc.tag @@ Id.of_string "Type") in
- let v_ty = process_expr env ty_expr ty in
+ let v_ty = set_of_type env ty in
let s = Id.Set.union v_ty (process_expr env e ty) in
Id.Set.elements s
diff --git a/vernac/proof_using.mli b/vernac/proof_using.mli
index ddab2742d..f63c8e242 100644
--- a/vernac/proof_using.mli
+++ b/vernac/proof_using.mli
@@ -14,8 +14,6 @@ val process_expr :
val name_set : Names.Id.t -> Vernacexpr.section_subset_expr -> unit
-val to_string : Vernacexpr.section_subset_expr -> string
-
val suggest_constant : Environ.env -> Names.Constant.t -> unit
val suggest_variable : Environ.env -> Names.Id.t -> unit