diff options
author | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-04 18:10:48 +0000 |
---|---|---|
committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-08-04 18:10:48 +0000 |
commit | 7d515acbc5d83aa2300b71a9b7712b3da1d3d2e3 (patch) | |
tree | 01b9d71f3982ebee13c41cd9c2d5d6960c317eee /proofs/refiner.ml | |
parent | 0721090dea4d9018f4c4cad8cefa1a10fb0d5a71 (diff) |
Évolutions diverses et variées.
- 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
Diffstat (limited to 'proofs/refiner.ml')
-rw-r--r-- | proofs/refiner.ml | 27 |
1 files changed, 13 insertions, 14 deletions
diff --git a/proofs/refiner.ml b/proofs/refiner.ml index 1ad7dcd0a..0014e9f72 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -189,7 +189,6 @@ let leaf g = let check_subproof_connection gl spfl = list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl - let abstract_operation syntax semantics gls = let (sgl_sigma,validation) = semantics gls in let hidden_proof = validation (List.map leaf sgl_sigma.it) in @@ -204,6 +203,7 @@ let abstract_tactic_expr ?(dflt=false) te tacfun gls = abstract_operation (Tactic(te,dflt)) tacfun gls let abstract_tactic ?(dflt=false) te = + !abstract_tactic_box := Some te; abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te)) let abstract_extended_tactic ?(dflt=false) s args = @@ -491,13 +491,18 @@ let tclNOTSAMEGOAL (tac : tactic) goal = (str"Tactic generated a subgoal identical to the original goal.") else rslt -let catch_failerror = function - | e when catchable_exception e -> check_for_interrupt () - | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) -> +let catch_failerror e = + if catchable_exception e then check_for_interrupt () + else match e with + | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) + | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_))) -> check_for_interrupt () | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located (s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) + | Stdpp.Exc_located(s,FailError (lvl,s')) -> + raise (Stdpp.Exc_located(s,FailError (lvl - 1, s'))) + | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s'))) -> + raise + (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s')))) | e -> raise e (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *) @@ -548,14 +553,8 @@ let ite_gen tcal tac_if continue tac_else gl= try tcal tac_if0 continue gl with (* Breakpoint *) - | e when catchable_exception e -> - check_for_interrupt (); tac_else0 e gl - | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e -> - check_for_interrupt (); tac_else0 e gl - | FailError (lvl,s) -> raise (FailError (lvl - 1, s)) - | Stdpp.Exc_located (s,FailError (lvl,s')) -> - raise (Stdpp.Exc_located (s,FailError (lvl - 1, s'))) - + | e -> catch_failerror e; tac_else0 e gl + (* Try the first tactic and, if it succeeds, continue with the second one, and if it fails, use the third one *) |