diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-05 20:44:17 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2014-02-05 20:44:17 +0100 |
| commit | 8089dc960c9e8caf778907fd87be48d77b066433 (patch) | |
| tree | a8ba14f89ede9edf5999673a5b31c3178f5d570f /grammar | |
| parent | 550378a5897b334ed3b9e64715e94de3893406dc (diff) | |
Tactic extensions do not need to be classified by the STM, as
they never produce a VernacExtend entry.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/tacextend.ml4 | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index e648aef4e..f96b67f5e 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -70,24 +70,6 @@ let make_fun_clauses loc s l = check_unicity s l; Compat.make_fun loc (List.map make_clause l) -let make_clause_classifier cg s (pt,c,_) = - match c ,cg with - | Some c, _ -> - (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr c) pt)), - make_let true c pt) - | None, Some cg -> - (make_patt pt, - vala (Some (make_when (MLast.loc_of_expr cg) pt)), - <:expr< fun () -> $cg$ $str:s$ >>) - | None, None -> - (make_patt pt, - vala (Some (make_when loc pt)), - <:expr< fun () -> (Vernacexpr.VtProofStep, Vernacexpr.VtLater) >>) - -let make_fun_classifiers loc s c l = - Compat.make_fun loc (List.map (make_clause_classifier c s) l) - let rec make_args = function | [] -> <:expr< [] >> | GramNonTerminal(loc,t,_,Some p)::l -> @@ -186,8 +168,6 @@ let declare_tactic loc s c cl = [ <:str_item< do { try do { Tacenv.register_ml_tactic $se$ $make_fun_clauses loc s cl$; - Vernac_classifier.declare_vernac_classifier - $se$ $make_fun_classifiers loc s c cl$; List.iter (fun (s,l) -> match l with [ Some l -> |