diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-09 23:38:00 +0100 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2015-12-10 17:44:19 +0100 |
commit | fb77937a6ba0fe45e978911db08de57f931683e1 (patch) | |
tree | 7a82660e8a0686d4989a615bf5c839ec2e7d8c60 | |
parent | 20e1829ad3de42dd322af972c6f9a585f40738ef (diff) |
Changing syntax of pat/constr1.../constrn into pat%constr1...%constrn.
Marking it as experimental.
-rw-r--r-- | CHANGES | 3 | ||||
-rw-r--r-- | doc/refman/RefMan-tac.tex | 14 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 3 | ||||
-rw-r--r-- | test-suite/success/intros.v | 20 | ||||
-rw-r--r-- | theories/Logic/WKL.v | 6 | ||||
-rw-r--r-- | theories/Logic/WeakFan.v | 2 | ||||
-rw-r--r-- | theories/Wellfounded/Lexicographic_Exponentiation.v | 2 |
7 files changed, 27 insertions, 23 deletions
@@ -9,6 +9,9 @@ Tactics - Syntax "destruct !hyp" changed to "destruct (hyp)", and similarly for induction. +- Syntax "p/c" for on-the-fly application of a lemma c before + introducing along pattern p changed to p%c1..%cn. The feature and + syntax are in experimental stage. Changes from V8.5beta2 to V8.5beta3 =================================== diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index f367f04c4..3a3877105 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -813,7 +813,7 @@ either: \item the pattern \texttt{?\ident} \item an identifier \end{itemize} -\item a {\em destructing introduction pattern} which itself classifies into: +\item an {\em action introduction pattern} which itself classifies into: \begin{itemize} \item a {\em disjunctive/conjunctive introduction pattern}, i.e. either one of: \begin{itemize} @@ -828,9 +828,9 @@ either: \item a pattern for decomposing an equality: {\tt [= $p_1$ \dots\ $p_n$]} \item the rewriting orientations: {\tt ->} or {\tt <-} \end{itemize} - \item the on-the-fly application of lemmas: $p${\tt /{\term$_1$}} - \ldots {\tt /{\term$_n$}} where $p$ itself is not an on-the-fly - application of lemmas pattern + \item the on-the-fly application of lemmas: $p${\tt \%{\term$_1$}} + \ldots {\tt \%{\term$_n$}} where $p$ itself is not a pattern for + on-the-fly application of lemmas (note: syntax is in experimental stage) \end{itemize} \item the wildcard: {\tt \_} \end{itemize} @@ -898,10 +898,10 @@ introduction pattern~$p$: itself is erased; if the term to substitute is a variable, it is substituted also in the context of goal and the variable is removed too; -\item introduction over a pattern $p${\tt /{\term$_1$}} \ldots {\tt - /{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the +\item introduction over a pattern $p${\tt \%{\term$_1$}} \ldots {\tt + \%{\term$_n$}} first applies {\term$_1$},\ldots, {\term$_n$} on the hypothesis to be introduced (as in {\tt apply }{\term}$_1$, \ldots, - {\term}$_n$ {\tt in}), prior to the application of the introduction + {\term}$_n$ {\tt in}) prior to the application of the introduction pattern $p$; \item introduction on the wildcard depends on whether the product is dependent or not: in the non-dependent case, it erases the diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 4d42dfe85..3d59b9b8d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -311,7 +311,8 @@ GEXTEND Gram | "**" -> !@loc, IntroForthcoming false ]] ; simple_intropattern: - [ [ pat = simple_intropattern_closed; l = LIST0 ["/"; c = constr -> c] -> + [ [ pat = simple_intropattern_closed; + l = LIST0 ["%"; c = operconstr LEVEL "0" -> c] -> let loc0,pat = pat in let f c pat = let loc = Loc.merge loc0 (Constrexpr_ops.constr_loc c) in diff --git a/test-suite/success/intros.v b/test-suite/success/intros.v index 741f372ff..17f160f98 100644 --- a/test-suite/success/intros.v +++ b/test-suite/success/intros.v @@ -34,47 +34,47 @@ intros _ ?. exact H. Qed. -(* A short test about introduction pattern pat/c *) +(* A short test about introduction pattern pat%c *) Goal (True -> 0=0) -> True /\ False -> 0=0. -intros H (H1/H,_). +intros H (H1%H,_). exact H1. Qed. (* A test about bugs in 8.5beta2 *) Goal (True -> 0=0) -> True /\ False -> False -> 0=0. intros H H0 H1. -destruct H0 as (a/H,_). +destruct H0 as (a%H,_). (* Check that H0 is removed (was bugged in 8.5beta2) *) Fail clear H0. -(* Check position of newly created hypotheses when using pat/c (was +(* Check position of newly created hypotheses when using pat%c (was left at top in 8.5beta2) *) match goal with H:_ |- _ => clear H end. (* clear H1:False *) match goal with H:_ |- _ => exact H end. (* check that next hyp shows 0=0 *) Qed. Goal (True -> 0=0) -> True -> 0=0. -intros H H1/H. +intros H H1%H. exact H1. Qed. Goal forall n, n = S n -> 0=0. -intros n H/n_Sn. +intros n H%n_Sn. destruct H. Qed. (* Another check about generated names and cleared hypotheses with - pat/c patterns *) + pat%c patterns *) Goal (True -> 0=0 /\ 1=1) -> True -> 0=0. -intros H (H1,?)/H. +intros H (H1,?)%H. change (1=1) in H0. exact H1. Qed. -(* Checking iterated pat/c1.../cn introduction patterns and side conditions *) +(* Checking iterated pat%c1...%cn introduction patterns and side conditions *) Goal forall A B C D:Prop, (A -> B -> C) -> (C -> D) -> B -> A -> D. intros * H H0 H1. -intros H2/H/H0. +intros H2%H%H0. - exact H2. - exact H1. Qed. 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 (). |