diff options
| author | letouzey | 2012-07-09 18:17:58 +0000 |
|---|---|---|
| committer | letouzey | 2012-07-09 18:17:58 +0000 |
| commit | f3870c96a192ff52449db9695b1c160834ff023f (patch) | |
| tree | c5b02c6e9a12df51ce7ca5005e0bdf0c58d74cec /grammar | |
| parent | 06d096b3ff3dff8cca216091c0c5ffa3a7530e1d (diff) | |
induction/destruct : nicer syntax for generating equations (solves #2741)
The ugly syntax "destruct x as [ ]_eqn:H" is replaced by:
destruct x eqn:H
destruct x as [ ] eqn:H
Some with induction. Of course, the pattern behind "as" is arbitrary.
For an anonymous version, H could be replaced by ?. The old syntax
with "_eqn" still works for the moment, by triggers a warning.
For making this new syntax work, we had to change the seldom-used
"induction x y z using foo" into "induction x, y, z using foo".
Now, only one "using" can be used per command instead of one per
comma-separated group earlier, but I doubt this will bother anyone.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15566 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index c202664e23..3c646c03af 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -359,13 +359,15 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_quantified_hypothesis h$ >> | Tacexpr.TacInductionDestruct (isrec,ev,l) -> <:expr< Tacexpr.TacInductionDestruct $mlexpr_of_bool isrec$ $mlexpr_of_bool ev$ - $mlexpr_of_pair (mlexpr_of_list (mlexpr_of_triple - (mlexpr_of_list mlexpr_of_induction_arg) - (mlexpr_of_option mlexpr_of_constr_with_binding) - (mlexpr_of_pair - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) - (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) - (mlexpr_of_option mlexpr_of_clause) l$ >> + $mlexpr_of_triple + (mlexpr_of_list + (mlexpr_of_pair + mlexpr_of_induction_arg + (mlexpr_of_pair + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern)) + (mlexpr_of_option (mlexpr_of_located mlexpr_of_intro_pattern))))) + (mlexpr_of_option mlexpr_of_constr_with_binding) + (mlexpr_of_option mlexpr_of_clause) l$ >> (* Context management *) | Tacexpr.TacClear (b,l) -> |