diff options
| author | coqbot-app[bot] | 2021-01-26 11:08:28 +0000 |
|---|---|---|
| committer | GitHub | 2021-01-26 11:08:28 +0000 |
| commit | 1a84bed789697ff9b4f5c70dec3c732cdbbdbce0 (patch) | |
| tree | 85cbefe72ebbeaa9b3d6c1c27545864f96faa245 /theories | |
| parent | 14051337936db1f56dc052a6e54e5b606552141b (diff) | |
| parent | 7ea0db435910c2db2a9ae4cadfd54f49f3640b62 (diff) | |
Merge PR #13758: Remove the Hide Obligations flag (deprecated in 8.12)
Reviewed-by: SkySkimmer
Reviewed-by: Zimmi48
Diffstat (limited to 'theories')
| -rw-r--r-- | theories/Program/Tactics.v | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index fce69437d7..d852ad24fe 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -319,7 +319,3 @@ Create HintDb program discriminated. Ltac program_simpl := program_simplify ; try typeclasses eauto 10 with program ; try program_solve_wf. Obligation Tactic := program_simpl. - -Definition obligation (A : Type) {a : A} := a. - -Register obligation as program.tactics.obligation. |