module DTI = DoubleTypeInference
module FNG = FreshNamesGenerator
-let debug = true
+let debug = false
let debug_print =
if debug then (fun x -> prerr_endline (Lazy.force x)) else (fun _ -> ())
in
PET.mk_tactic subst_tac
-and destruct ?(simplified = false) ~first_time term =
+and destruct ~first_time term =
let are_convertible hd1 hd2 metasenv context =
fst (CR.are_convertible ~metasenv context hd1 hd2 CU.empty_ugraph)
in
| _, C.Rel i2 when DTI.does_not_occur i2 t1 ->
mk_subst_chain `RightToLeft i2 t1 t2
(* else part *)
- | _ when first_time && simplified -> raise exn_nothingtodo
- | _ when simplified (* && not first time *) -> T.id_tac
- | _ (* when not simplified *) ->
- T.then_ ~start:(simpl_in_term context term)
- ~continuation:(destruct ~simplified:true ~first_time term)
+ | _ when first_time -> raise exn_nothingtodo
+ | _ (* when not first time *) -> T.id_tac
end
- | _ when first_time && simplified -> raise exn_nothingtodo
- | _ when simplified (* && not first time *) -> T.id_tac
- | _ (* when not simplified *) ->
- T.then_ ~start:(simpl_in_term context term)
- ~continuation:(destruct ~simplified:true ~first_time term)
+ | _ when first_time -> raise exn_nothingtodo
+ | _ (* when not first time *) -> T.id_tac
in
PET.apply_tactic tac status
in