diff options
Diffstat (limited to 'proofs/proof_using.ml')
| -rw-r--r-- | proofs/proof_using.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml index a69645b11..681a7fa1a 100644 --- a/proofs/proof_using.ml +++ b/proofs/proof_using.ml @@ -10,6 +10,7 @@ open Names open Environ open Util open Vernacexpr +open Context.Named.Declaration let to_string e = let rec aux = function @@ -33,7 +34,8 @@ let in_nameset = let rec close_fwd e s = let s' = - List.fold_left (fun s (id,b,ty) -> + List.fold_left (fun s decl -> + let (id,b,ty) = Context.Named.Declaration.to_tuple decl in let vb = Option.(default Id.Set.empty (map (global_vars_set e) b)) in let vty = global_vars_set e ty in let vbty = Id.Set.union vb vty in @@ -61,13 +63,13 @@ and set_of_id env ty id = Id.Set.union (global_vars_set env ty) acc) Id.Set.empty ty else if Id.to_string id = "All" then - List.fold_right Id.Set.add (List.map pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map 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 pi1 (named_context env)) Id.Set.empty + List.fold_right Id.Set.add (List.map get_id (named_context env)) Id.Set.empty let process_expr env e ty = let ty_expr = SsSingl(Loc.ghost, Id.of_string "Type") in |