diff options
| author | Pierre-Marie Pédrot | 2019-02-04 15:00:13 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2019-02-04 15:00:13 +0100 |
| commit | 79c87ab3ec6e41bbc5fe2cc43edcb4b934b81e46 (patch) | |
| tree | 18ce7b34d9865b5c4446f1ff6505e6682c80650c /theories/Program/Subset.v | |
| parent | 127f1fe146264a87d7a8cb04ab8ea34201b5c93a (diff) | |
| parent | f53a011ac83fa820faba970109485780715e153f (diff) | |
Merge PR #9386: Pass some files to strict focusing mode.
Reviewed-by: Zimmi48
Reviewed-by: herbelin
Reviewed-by: ppedrot
Diffstat (limited to 'theories/Program/Subset.v')
| -rw-r--r-- | theories/Program/Subset.v | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 1c89b6c3b1..ae366204ac 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -73,10 +73,10 @@ Proof. simpl. split ; intros ; subst. - inversion H. - reflexivity. + - inversion H. + reflexivity. - pi. + - pi. Qed. (* Somewhat trivial definition, but not unfolded automatically hence we can match on [match_eq ?A ?B ?x ?f] |