diff options
Diffstat (limited to 'ltac/tauto.ml')
| -rw-r--r-- | ltac/tauto.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/ltac/tauto.ml b/ltac/tauto.ml index 11996af73..e3f5342de 100644 --- a/ltac/tauto.ml +++ b/ltac/tauto.ml @@ -161,8 +161,9 @@ let flatten_contravariant_conj _ ist = | Some (_,args) -> let args = List.map EConstr.Unsafe.to_constr args in let newtyp = List.fold_right mkArrow args c in + let newtyp = EConstr.of_constr newtyp in let intros = tclMAP (fun _ -> intro) args in - let by = tclTHENLIST [intros; apply hyp; split; assumption] in + let by = tclTHENLIST [intros; apply (EConstr.of_constr hyp); split; assumption] in tclTHENLIST [assert_ ~by newtyp; clear (destVar hyp)] | _ -> fail @@ -186,17 +187,17 @@ let flatten_contravariant_disj _ ist = let typ = assoc_var "X1" ist in let typ = EConstr.of_constr typ in let c = assoc_var "X2" ist in + let c = EConstr.of_constr c in let hyp = assoc_var "id" ist in match match_with_disjunction sigma ~strict:flags.strict_in_contravariant_hyp ~onlybinary:flags.binary_mode typ with | Some (_,args) -> - let args = List.map EConstr.Unsafe.to_constr args in let map i arg = - let typ = mkArrow arg c in + let typ = EConstr.mkArrow arg c in let ci = Tactics.constructor_tac false None (succ i) Misctypes.NoBindings in - let by = tclTHENLIST [intro; apply hyp; ci; assumption] in + let by = tclTHENLIST [intro; apply (EConstr.of_constr hyp); ci; assumption] in assert_ ~by typ in let tacs = List.mapi map args in @@ -231,6 +232,7 @@ let apply_nnpp _ ist = (Proofview.tclUNIT ()) begin fun () -> try let nnpp = Universes.constr_of_global (Nametab.global_of_path coq_nnpp_path) in + let nnpp = EConstr.of_constr nnpp in apply nnpp with Not_found -> tclFAIL 0 (Pp.mt ()) end |