diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2014-10-14 16:30:34 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-10-14 16:30:34 +0200 |
| commit | 5ce9a1ab622c9b6982a42e8d5cd217787eea8745 (patch) | |
| tree | 643354c34716c4426e347a93811a5ae38aa729b8 /pretyping | |
| parent | a0f3e1fe045d069cb28af21e88ea60d6b3b79c74 (diff) | |
Oops, forgot a fix needed after the rebase.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/unification.ml | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 64d837f0c..6f846d2e0 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -549,16 +549,6 @@ let eta_constructor_app env f l1 term = | _ -> assert false) | _ -> assert false -let debug_unification = ref (false) -let _ = Goptions.declare_bool_option { - Goptions.optsync = true; Goptions.optdepr = false; - Goptions.optname = - "Print states sent to w_unify unification"; - Goptions.optkey = ["Debug";"Tactic";"Unification"]; - Goptions.optread = (fun () -> !debug_unification); - Goptions.optwrite = (fun a -> debug_unification:=a); -} - let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb flags m n = let rec unirec_rec (curenv,nb as curenvnb) pb opt ((sigma,metasubst,evarsubst) as substn) curm curn = let cM = Evarutil.whd_head_evar sigma curm |