diff options
| author | Pierre-Marie Pédrot | 2015-12-24 17:55:25 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-12-24 18:24:34 +0100 |
| commit | daa7cb065a238c7d4ee394e00315d66d023e5259 (patch) | |
| tree | d50643d775bca154f7ea422786b6d835e48d09fa /grammar | |
| parent | f33fc85b1dd2f4994dc85b0943fe503ace2cc5ff (diff) | |
Removing auto from the tactic AST.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/q_coqast.ml4 | 13 |
1 files changed, 0 insertions, 13 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4 index 7001f5f627..fc08f0a492 100644 --- a/grammar/q_coqast.ml4 +++ b/grammar/q_coqast.ml4 @@ -420,19 +420,6 @@ let rec mlexpr_of_atomic_tactic = function (* Equivalence relations *) | Tacexpr.TacSymmetry ido -> <:expr< Tacexpr.TacSymmetry $mlexpr_of_clause ido$ >> - (* Automation tactics *) - | Tacexpr.TacAuto (debug,n,lems,l) -> - let d = mlexpr_of_debug debug in - let n = mlexpr_of_option (mlexpr_of_or_var mlexpr_of_int) n in - let lems = mlexpr_of_list mlexpr_of_constr lems in - let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in - <:expr< Tacexpr.TacAuto $d$ $n$ $lems$ $l$ >> - | Tacexpr.TacTrivial (debug,lems,l) -> - let d = mlexpr_of_debug debug in - let l = mlexpr_of_option (mlexpr_of_list mlexpr_of_string) l in - let lems = mlexpr_of_list mlexpr_of_constr lems in - <:expr< Tacexpr.TacTrivial $d$ $lems$ $l$ >> - | _ -> failwith "Quotation of atomic tactic expressions: TODO" and mlexpr_of_tactic : (Tacexpr.raw_tactic_expr -> MLast.expr) = function |