aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-09 23:38:00 +0100
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2015-12-10 17:44:19 +0100
commitfb77937a6ba0fe45e978911db08de57f931683e1 (patch)
tree7a82660e8a0686d4989a615bf5c839ec2e7d8c60 /theories
parent20e1829ad3de42dd322af972c6f9a585f40738ef (diff)
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Marking it as experimental.
Diffstat (limited to 'theories')
-rw-r--r--theories/Logic/WKL.v6
-rw-r--r--theories/Logic/WeakFan.v2
-rw-r--r--theories/Wellfounded/Lexicographic_Exponentiation.v2
3 files changed, 5 insertions, 5 deletions
diff --git a/theories/Logic/WKL.v b/theories/Logic/WKL.v
index 408eca4a3..abe6a8d99 100644
--- a/theories/Logic/WKL.v
+++ b/theories/Logic/WKL.v
@@ -40,7 +40,7 @@ Proposition is_path_from_characterization P n l :
Proof.
intros. split.
- induction 1 as [|* HP _ (l'&Hl'&HPl')|* HP _ (l'&Hl'&HPl')].
- + exists []. split. reflexivity. intros n <-/le_n_0_eq. assumption.
+ + exists []. split. reflexivity. intros n <-%le_n_0_eq. assumption.
+ exists (true :: l'). split. apply eq_S, Hl'. intros [|] H.
* assumption.
* simpl. rewrite <- app_assoc. apply HPl', le_S_n, H.
@@ -51,10 +51,10 @@ intros. split.
+ constructor. apply (HPl' 0). apply le_0_n.
+ eapply next_left.
* apply (HPl' 0), le_0_n.
- * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+ * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+ apply next_right.
* apply (HPl' 0), le_0_n.
- * fold (length l'). apply IHl'. intros n' H/le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
+ * fold (length l'). apply IHl'. intros n' H%le_n_S. apply HPl' in H. simpl in H. rewrite <- app_assoc in H. assumption.
Qed.
(** [infinite_from P l] means that we can find arbitrary long paths
diff --git a/theories/Logic/WeakFan.v b/theories/Logic/WeakFan.v
index 2f84ebe5f..365661be0 100644
--- a/theories/Logic/WeakFan.v
+++ b/theories/Logic/WeakFan.v
@@ -89,7 +89,7 @@ Qed.
Theorem WeakFanTheorem : forall P, barred P -> inductively_barred P [].
Proof.
intros P Hbar.
-destruct Hbar with (X P) as (l,(Hd/Y_approx,HP)).
+destruct Hbar with (X P) as (l,(Hd%Y_approx,HP)).
assert (inductively_barred P l) by (apply (now P l), HP).
clear Hbar HP.
induction l as [|a l].
diff --git a/theories/Wellfounded/Lexicographic_Exponentiation.v b/theories/Wellfounded/Lexicographic_Exponentiation.v
index dd9e4c986..b8b9e929c 100644
--- a/theories/Wellfounded/Lexicographic_Exponentiation.v
+++ b/theories/Wellfounded/Lexicographic_Exponentiation.v
@@ -95,7 +95,7 @@ Section Wf_Lexicographic_Exponentiation.
intros.
- inversion H.
assert ([b; a] = ([] ++ [b]) ++ [a]) by auto with sets.
- destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)/app_inj_tail, <-).
+ destruct (app_inj_tail (l ++ [y]) ([] ++ [b]) _ _ H0) as ((?, <-)%app_inj_tail, <-).
inversion H1; subst; [ apply rt_step; assumption | apply rt_refl ].
- inversion H0.
+ apply app_cons_not_nil in H3 as ().