diff options
| author | Hugo Herbelin | 2014-08-03 19:18:21 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-08-05 19:52:22 +0200 |
| commit | 262e3151ce483aaab3b4f60e3d1dbdf875ea05ae (patch) | |
| tree | 75d664dd62bb332cd3e8203c39e748102e0b2a57 /grammar | |
| parent | 8b8f8efe356a190ed2ae70b42688ef9170ef13b2 (diff) | |
Experimentally adding an option for automatically erasing an
hypothesis when using it in apply or rewrite (prefix ">",
undocumented), and a modifier to explicitly keep it in induction or
destruct (prefix "!", reminiscent of non-linerarity).
Also added undocumented option "Set Default Clearing Used Hypotheses"
which makes apply and rewrite default to erasing the hypothesis they
use (if ever their argument is indeed an hypothesis of the context).
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 2690cf8670..4fede761f4 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -247,6 +247,9 @@ let mlexpr_of_binding = mlexpr_of_pair mlexpr_of_binding_kind mlexpr_of_constr let mlexpr_of_constr_with_binding = mlexpr_of_pair mlexpr_of_constr mlexpr_of_binding_kind +let mlexpr_of_constr_with_binding_arg = + mlexpr_of_pair (mlexpr_of_option mlexpr_of_bool) mlexpr_of_constr_with_binding + let mlexpr_of_move_location f = function | Misctypes.MoveAfter id -> <:expr< Misctypes.MoveAfter $f id$ >> | Misctypes.MoveBefore id -> <:expr< Misctypes.MoveBefore $f id$ >> @@ -309,13 +312,13 @@ let rec mlexpr_of_atomic_tactic = function | Tacexpr.TacExact c -> <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> | Tacexpr.TacApply (b,false,cb,None) -> - <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding cb$ None >> + <:expr< Tacexpr.TacApply $mlexpr_of_bool b$ False $mlexpr_of_list mlexpr_of_constr_with_binding_arg cb$ None >> | Tacexpr.TacElim (false,cb,cbo) -> - let cb = mlexpr_of_constr_with_binding cb in + let cb = mlexpr_of_constr_with_binding_arg cb in let cbo = mlexpr_of_option mlexpr_of_constr_with_binding cbo in <:expr< Tacexpr.TacElim False $cb$ $cbo$ >> | Tacexpr.TacCase (false,cb) -> - let cb = mlexpr_of_constr_with_binding cb in + let cb = mlexpr_of_constr_with_binding_arg cb in <:expr< Tacexpr.TacCase False $cb$ >> | Tacexpr.TacFix (ido,n) -> let ido = mlexpr_of_ident_option ido in @@ -364,7 +367,9 @@ let rec mlexpr_of_atomic_tactic = function $mlexpr_of_triple (mlexpr_of_list (mlexpr_of_pair - mlexpr_of_induction_arg + (mlexpr_of_pair + (mlexpr_of_option mlexpr_of_bool) + 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))))) |