From 7d515acbc5d83aa2300b71a9b7712b3da1d3d2e3 Mon Sep 17 00:00:00 2001 From: herbelin Date: Mon, 4 Aug 2008 18:10:48 +0000 Subject: Évolutions diverses et variées. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit - Correction divers messages d'erreur - lorsque rien à réécrire dans une hyp, - lorsqu'une variable ltac n'est pas liée, - correction anomalie en présence de ?id dans le "as" de induction, - correction mauvais env dans message d'erreur de unify_0. - Diverses extensions et améliorations - "specialize" : - extension au cas (fun x1 ... xn => H u1 ... un), - renommage au même endroit. - "assert" et "pose proof" peuvent réutiliser la même hyp comme "specialize". - "induction" - intro des IH toujours au sommet même si induction sur var quantifiée, - ajout d'un hack pour la reconnaissance de schémas inductifs comme N_ind_double mais il reste du boulot pour reconnaître (et/ou réordonner) les composantes d'un schéma dont les hypothèses ne sont pas dans l'ordre standard, - vérification de longueur et éventuelle complétion des intropatterns dans le cas de sous-patterns destructifs dans induction (par exemple "destruct n as [|[|]]" sur "forall n, n=0" ne mettait pas le n dans le contexte), - localisation des erreurs d'intropattern, - ajout d'un pattern optionnel après "as" pour forcer une égalité et la nommer (*). - "apply" accepte plusieurs arguments séparés par des virgules (*). - Plus de robustesse pour clear en présence d'evars. - Amélioration affichage TacFun dans Print Ltac. - Vieux pb espace en trop en tête d'affichage des tactiques EXTEND résolu (incidemment, ça remodifie une nouvelle fois le test output Fixpoint.v !). - Fusion VTactic/VFun dans l'espoir. - Mise en place d'un système de trace de la pile des appels Ltac (tout en préservant certains aspects de la récursivité terminale - cf bug #468). - Tactiques primitives - ajout de "move before" dans les tactiques primitives et ajout des syntaxes move before et move dependent au niveau utilisateur (*), - internal_cut peuvent faire du remplacement de nom d'hypothèse existant, - suppression de Intro_replacing et du code sous-traitant - Nettoyage - Suppression cible et fichiers minicoq non portés depuis longtemps. (*) Extensions de syntaxe qu'il pourrait être opportun de discuter git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11300 85f007b7-540e-0410-9357-904b9bb8a0f7 --- tactics/hiddentac.mli | 31 +++++++++++++++++++------------ 1 file changed, 19 insertions(+), 12 deletions(-) (limited to 'tactics/hiddentac.mli') diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index bb88518c9..8d15f864c 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -10,6 +10,7 @@ (*i*) open Names +open Util open Term open Proof_type open Tacmach @@ -25,7 +26,7 @@ open Clenv (* Basic tactics *) -val h_intro_move : identifier option -> identifier option -> tactic +val h_intro_move : identifier option -> identifier move_location -> tactic val h_intro : identifier -> tactic val h_intros_until : quantified_hypothesis -> tactic @@ -35,7 +36,7 @@ val h_exact_no_check : constr -> tactic val h_vm_cast_no_check : constr -> tactic val h_apply : advanced_flag -> evars_flag -> - constr with_ebindings -> tactic + constr with_ebindings list -> tactic val h_elim : evars_flag -> constr with_ebindings -> constr with_ebindings option -> tactic @@ -63,14 +64,20 @@ val h_instantiate : int -> Rawterm.rawconstr -> val h_simple_induction : quantified_hypothesis -> tactic val h_simple_destruct : quantified_hypothesis -> tactic -val h_new_induction : - evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> - Tacticals.clause option -> tactic -val h_new_destruct : - evars_flag -> constr with_ebindings induction_arg list -> - constr with_ebindings option -> intro_pattern_expr -> - Tacticals.clause option -> tactic +val h_simple_induction_destruct : rec_flag -> quantified_hypothesis -> tactic +val h_new_induction : evars_flag -> + constr with_ebindings induction_arg list -> constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + Tacticals.clause option -> tactic +val h_new_destruct : evars_flag -> + constr with_ebindings induction_arg list -> constr with_ebindings option -> + intro_pattern_expr located option * intro_pattern_expr located option -> + Tacticals.clause option -> tactic +val h_induction_destruct : rec_flag -> evars_flag -> + (constr with_ebindings induction_arg list * constr with_ebindings option * + (intro_pattern_expr located option * intro_pattern_expr located option) * + Tacticals.clause option) list -> tactic + val h_specialize : int option -> constr with_ebindings -> tactic val h_lapply : constr -> tactic @@ -80,7 +87,7 @@ val h_lapply : constr -> tactic (* Context management *) val h_clear : bool -> identifier list -> tactic val h_clear_body : identifier list -> tactic -val h_move : bool -> identifier -> identifier -> tactic +val h_move : bool -> identifier -> identifier move_location -> tactic val h_rename : (identifier*identifier) list -> tactic val h_revert : identifier list -> tactic @@ -110,4 +117,4 @@ val h_simplest_eapply : constr -> tactic val h_simplest_elim : constr -> tactic val h_simplest_case : constr -> tactic -val h_intro_patterns : intro_pattern_expr list -> tactic +val h_intro_patterns : intro_pattern_expr located list -> tactic -- cgit v1.2.3