diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-16 17:01:42 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-05-16 17:14:55 +0200 |
| commit | e321cfd21e28161923b84d943cb15c6d775b0d9e (patch) | |
| tree | f9acbdf0bf8c7ba8cf12b7282c6af700d8d7408f /grammar | |
| parent | c2f78ed4fba9fa027fdf2051f214e1c5b4fe670e (diff) | |
Moving argument-free tactics out of the AST into a dedicated
"coretactics.ml4" file.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 3 |
1 files changed, 0 insertions, 3 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 9a0a22b9f..abc0d31a9 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -308,8 +308,6 @@ let rec mlexpr_of_atomic_tactic = function let idopt = mlexpr_of_ident_option idopt in let idopt'= mlexpr_of_move_location mlexpr_of_hyp idopt' in <:expr< Tacexpr.TacIntroMove $idopt$ $idopt'$ >> - | Tacexpr.TacAssumption -> - <:expr< Tacexpr.TacAssumption >> | Tacexpr.TacExact c -> <:expr< Tacexpr.TacExact $mlexpr_of_constr c$ >> | Tacexpr.TacExactNoCheck c -> @@ -420,7 +418,6 @@ let rec mlexpr_of_atomic_tactic = function <:expr< Tacexpr.TacChange $g p$ $mlexpr_of_constr c$ $l$ >> (* Equivalence relations *) - | Tacexpr.TacReflexivity -> <:expr< Tacexpr.TacReflexivity >> | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> | Tacexpr.TacTransitivity c -> <:expr< Tacexpr.TacTransitivity $mlexpr_of_option mlexpr_of_constr c$ >> |