小编Tom*_*Tom的帖子

我在本地提交了一些更改，然后将它们推送到github。我去了github网站，我可以看到我刚刚推送的提交。

几个小时后，当我返回 github 时，我所做的提交丢失了。我如何知道这些提交会发生什么？为什么它们不再出现在 github 上？我如何知道我的同事是否删除或重置了它？我可以在 github 上找到我身后所做的提交，但这些新提交与我的提交和我所做更改的代码无关。

ps 我有那些丢失的提交的提交 ID。

我想写一个带有可选变量名的策略.最初的战术看起来像这样:

Require Import Classical.

Ltac save := 
  let H := fresh in
  apply NNPP;
  intro H;
  apply H.

我想让用户有机会选择他想要的名字,并使用它:save a例如.

我用这个解决方案编写了一个变体:

Require Import Classical.

Inductive ltac_No_arg : Set :=
  | ltac_no_arg : ltac_No_arg.

Ltac savetactic h := 
  match type of h with
    | ltac_No_arg => let H := fresh in
      apply NNPP;
      intro H;
      apply H
    | _ => apply NNPP;
      intro h;
      apply h
  end.

Tactic Notation "save" := savetactic ltac_no_arg.
Tactic Notation …