diff options
Diffstat (limited to 'proofs/evar_refiner.ml')
| -rw-r--r-- | proofs/evar_refiner.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 456ce67e9..40c1f2906 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -25,14 +25,12 @@ type w_tactic = walking_constraints -> walking_constraints let local_Constraints lc gs = refiner (Local_constraints lc) gs -let debug = ref true;; - let startWalk gls = let evc = project_with_focus gls in let wc = (ids_mk evc) in (wc, (fun wc' gls' -> - if !debug & ids_eq wc wc' & gls.it = gls'.it then + if not !Options.debug or (ids_eq wc wc' & gls.it = gls'.it) then if Intset.equal (get_lc gls.it) (get_focus (ids_it wc')) then tclIDTAC {it=gls'.it; sigma = get_gc (ids_it wc')} else |