Imported Upstream version 8.8.2upstream/8.8.2

1 files changed, 0 insertions, 166 deletions

diff --git a/proofs/proof_using.ml b/proofs/proof_using.ml
deleted file mode 100644
index caa9b328..00000000
--- a/proofs/proof_using.ml
+++ /dev/null
@@ -1,166 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Environ
-open Util
-open Vernacexpr
-open 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 =
-  let open Libobject in
-  declare_object { (default_object "proofusing-nameset") with
-    cache_function = (fun (_,x) -> known_names := x :: !known_names);
-    classify_function = (fun _ -> Dispose);
-    discharge_function = (fun _ -> None)
-  }
-
-let rec close_fwd e s =
-  let s' =
-    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
-      if Id.Set.exists (fun v -> Id.Set.mem v s) vbty
-      then Id.Set.add id (Id.Set.union s vbty) else s)
-    s (named_context e)
-    in
-  if Id.Set.equal s s' then s else close_fwd e s'
-;;
-
-let rec process_expr env e ty =
-  let rec aux = function
-    | SsEmpty -> Id.Set.empty
-    | SsSingl (_,id) -> set_of_id env ty 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)
-  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
-    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 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
-  let v_ty = process_expr env ty_expr ty in
-  let s = Id.Set.union v_ty (process_expr env e ty) in
-  Id.Set.elements s
-
-let name_set id expr = Lib.add_anonymous_leaf (in_nameset (id,expr))
-
-let minimize_hyps env ids =
-  let rec aux ids =
-    let ids' =
-      Id.Set.fold (fun id alive ->
-        let impl_by_id =
-          Id.Set.remove id (really_needed env (Id.Set.singleton id)) in
-        if Id.Set.is_empty impl_by_id then alive
-        else Id.Set.diff alive impl_by_id)
-      ids ids in
-    if Id.Set.equal ids ids' then ids else aux ids'
-  in
-    aux ids
-
-let remove_ids_and_lets env s ids =
-  let not_ids id = not (Id.Set.mem id ids) in
-  let no_body id = named_body id env = None in
-  let deps id = really_needed env (Id.Set.singleton id) in
-    (Id.Set.filter (fun id ->
-      not_ids id &&
-     (no_body id ||
-       Id.Set.exists not_ids (Id.Set.filter no_body (deps id)))) s)
-
-let suggest_Proof_using name env vars ids_typ context_ids =
-  let module S = Id.Set in
-  let open Pp in
-  let print x = prerr_endline (string_of_ppcmds x) in
-  let pr_set parens s =
-    let wrap ppcmds =
-      if parens && S.cardinal s > 1 then str "(" ++ ppcmds ++ str ")"
-      else ppcmds in
-    wrap (prlist_with_sep (fun _ -> str" ") Id.print (S.elements s)) in
-  let used = S.union vars ids_typ in
-  let needed = minimize_hyps env (remove_ids_and_lets env used ids_typ) in
-  let all_needed = really_needed env needed in
-  let all = List.fold_right S.add context_ids S.empty in
-  let fwd_typ = close_fwd env ids_typ in
-  if !Flags.debug then begin
-    print (str "All "        ++ pr_set false all);
-    print (str "Type "       ++ pr_set false ids_typ);
-    print (str "needed "     ++ pr_set false needed);
-    print (str "all_needed " ++ pr_set false all_needed);
-    print (str "Type* "      ++ pr_set false fwd_typ);
-  end;
-  let valid_exprs = ref [] in
-  let valid e = valid_exprs := e :: !valid_exprs in
-  if S.is_empty needed then valid (str "Type");
-  if S.equal all_needed fwd_typ then valid (str "Type*");
-  if S.equal all all_needed then valid(str "All");
-  valid (pr_set false needed);
-  Feedback.msg_info (
-    str"The proof of "++ str name ++ spc() ++
-    str "should start with one of the following commands:"++spc()++
-    v 0 (
-    prlist_with_sep cut (fun x->str"Proof using " ++x++ str". ") !valid_exprs));
-  string_of_ppcmds (prlist_with_sep (fun _ -> str";")  (fun x->x) !valid_exprs)
-;;
-
-let value = ref false
-
-let _ =
-  Goptions.declare_bool_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "suggest Proof using";
-      Goptions.optkey   = ["Suggest";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      Goptions.optwrite = (fun b ->
-        value := b;
-        if b then Term_typing.set_suggest_proof_using suggest_Proof_using
-        else Term_typing.set_suggest_proof_using (fun _ _ _ _ _ -> "")
-      ) }
-
-let value = ref None
-
-let _ =
-  Goptions.declare_stringopt_option
-    { Goptions.optsync  = true;
-      Goptions.optdepr  = false;
-      Goptions.optname  = "default value for Proof using";
-      Goptions.optkey   = ["Default";"Proof";"Using"];
-      Goptions.optread  = (fun () -> !value);
-      Goptions.optwrite = (fun b -> value := b;) }
-
-
-let get_default_proof_using () = !value