diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/auto.ml | 1 | ||||
| -rw-r--r-- | tactics/equality.ml | 5 | ||||
| -rw-r--r-- | tactics/tactics.ml | 1 |
3 files changed, 0 insertions, 7 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index fd6dd0361..35b0dc7ff 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -1105,7 +1105,6 @@ si après Intros la conclusion matche le pattern. let (forward_interp_tactic, extern_interp) = Hook.make () -(* arnaud: potentiel bug avec ce try/with *) let conclPattern concl pat tac = let constr_bindings = match pat with diff --git a/tactics/equality.ml b/tactics/equality.ml index a7b04bee2..babc88944 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1550,9 +1550,6 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) = (* Look for an hypothesis hyp of the form "x=rhs" or "rhs=x", rewrite it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *) -(* arnaud: il va y avoir un bug là-dedans. Le try ne se déclenche pas - au bon endroit. Il faut convertir test en une Proofview.tactic - pour la gestion des exceptions. *) let subst_one_var dep_proof_ok x = Proofview.Goal.hyps >>= fun hyps -> let hyps = Environ.named_context_of_val hyps in @@ -1593,7 +1590,6 @@ let default_subst_tactic_flags () = else { only_leibniz = true; rewrite_dependent_proof = false } -(* arnaud: encore des erreurs potentiels avec ces try/with *) let subst_all ?(flags=default_subst_tactic_flags ()) = Tacmach.New.of_old find_eq_data_decompose >>= fun find_eq_data_decompose -> let test (_,c) = @@ -1639,7 +1635,6 @@ let cond_eq_term_left c t = Tacmach.New.of_old (cond_eq_term_left c t) let cond_eq_term_right c t = Tacmach.New.of_old (cond_eq_term_right c t) let cond_eq_term c t = Tacmach.New.of_old (cond_eq_term c t) -(* arnaud: toujours des histoires de try/with *) let rewrite_multi_assumption_cond cond_eq_term cl = let rec arec = function | [] -> error "No such assumption." diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 233e9f85b..5b1ae69e3 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -869,7 +869,6 @@ let find_eliminator c gl = let c = lookup_eliminator ind (elimination_sort_of_goal gl) in {elimindex = None; elimbody = (c,NoBindings)} -(* arnaud: probable bug avec le try *) let default_elim with_evars (c,_ as cx) = Proofview.tclORELSE (Tacmach.New.of_old (find_eliminator c) >>= fun elim -> |