From 04fb64e05365cb6eaf56baeffc72aa0b5d4b9a1b Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 5 Aug 2008 15:38:31 +0000 Subject: Correction de bugs: - evarconv: mauvaise idée d'utiliser la conversion sur la tête d'un terme applicatif au moment de tester f u1 .. un = g v1 .. vn au premier ordre : on revient sur l'algo tel qu'il était avant le commit 11187. - Bug #1887 (format récursif cassé à cause de la vérification des idents). - Nouveau choix de formattage du message "Tactic Failure". - Nettoyage vocabulaire "match context" -> "match goal" au passage. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11305 85f007b7-540e-0410-9357-904b9bb8a0f7 --- proofs/tacexpr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'proofs') diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index 34ddbb1893..29d7a7bb17 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -253,7 +253,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr = | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list - | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list + | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg -- cgit v1.2.3