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 | |
| 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')
| -rw-r--r-- | theories/Program/Subset.v | 6 | ||||
| -rw-r--r-- | theories/Program/Wf.v | 20 |
2 files changed, 13 insertions, 13 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] diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index f9d23e3cf6..092c1d6f48 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -97,15 +97,15 @@ Section Measure_well_founded. Proof with auto. unfold well_founded. cut (forall (a: M) (a0: T), m a0 = a -> Acc MR a0). - intros. + + intros. apply (H (m a))... - apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). - intros. - apply Acc_intro. - intros. - unfold MR in H1. - rewrite H0 in H1. - apply (H (m y))... + + apply (@well_founded_ind M R wf (fun mm => forall a, m a = mm -> Acc MR a)). + intros. + apply Acc_intro. + intros. + unfold MR in H1. + rewrite H0 in H1. + apply (H (m y))... Defined. End Measure_well_founded. @@ -245,8 +245,8 @@ Module WfExtensionality. intros ; apply Fix_eq ; auto. intros. assert(f = g). - extensionality y ; apply H. - rewrite H0 ; auto. + - extensionality y ; apply H. + - rewrite H0 ; auto. Qed. (** Tactic to unfold once a definition based on [Fix_sub]. *) |