diff options
| -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 e648aef4eb..f96b67f5e9 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 -> |