From 4dc7a3eb4ac669ead5ee4a1986c4a2310ffda911 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 19 Jan 2003 22:06:34 +0000
Subject: Restructuration interpréteur de tactique: plus d'évaluation partielle
 à la définition; suppression TacFunRec, VClosure, VFTactic et VContext;
 davantage de globalisation statique (notamment pour les tactiques
 mutuellement récursives); débogueur plus informatif

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3532 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/tacexpr.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs')

diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index dc163ea210..2761fbbdf8 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -193,7 +193,6 @@ and ('constr,'cst,'ind,'id) gen_tactic_expr =
   | TacMatch of constr_expr may_eval * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
   | TacMatchContext of direction_flag * (pattern_expr,('constr,'cst,'ind,'id) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'cst,'ind,'id) gen_tactic_fun_ast
-  | TacFunRec of (identifier located * ('constr,'cst,'ind,'id) gen_tactic_fun_ast)
   | TacArg of ('constr,'cst,'ind,'id) gen_tactic_arg
 
 and ('constr,'cst,'ind,'id) gen_tactic_fun_ast =
-- 
cgit v1.2.3