diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 6 | ||||
| -rw-r--r-- | plugins/ltac/profile_ltac.ml | 2 | ||||
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 1 |
3 files changed, 4 insertions, 5 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index ebeddf5f65..d335836dfc 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -156,7 +156,7 @@ let build_newrecursive let (rec_sign,rec_impls) = List.fold_left (fun (env,impls) (((_,recname),_),bl,arityc,_) -> - let arityc = Constrexpr_ops.prod_constr_expr arityc bl in + let arityc = Constrexpr_ops.mkCProdN Loc.ghost bl arityc in let arity,ctx = Constrintern.interp_type env0 sigma arityc in let evdref = ref (Evd.from_env env0) in let _, (_, impls') = Constrintern.interp_context_evars env evdref bl in @@ -453,7 +453,7 @@ let generate_correction_proof_wf f_ref tcc_lemma_ref let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas args ret_type body pre_hook = - let type_of_f = Constrexpr_ops.prod_constr_expr ret_type args in + let type_of_f = Constrexpr_ops.mkCProdN Loc.ghost args ret_type in let rec_arg_num = let names = List.map @@ -484,7 +484,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas Constrexpr.CApp (Loc.ghost,(None,Constrexpr_ops.mkRefC (Qualid (Loc.ghost,(qualid_of_string "Logic.eq")))), [(f_app_args,None);(body,None)]) in - let eq = Constrexpr_ops.prod_constr_expr unbounded_eq args in + let eq = Constrexpr_ops.mkCProdN Loc.ghost args unbounded_eq in let hook ((f_ref,_) as fconst) tcc_lemma_ref (functional_ref,_) (eq_ref,_) rec_arg_num rec_arg_type nb_args relation = try diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml index 58123f63ef..bcb28f77ce 100644 --- a/plugins/ltac/profile_ltac.ml +++ b/plugins/ltac/profile_ltac.ml @@ -374,7 +374,7 @@ let data = ref SM.empty let _ = Feedback.(add_feeder (function - | { id = State s; contents = Custom (_, "ltacprof_results", xml) } -> + | { id = s; contents = Custom (_, "ltacprof_results", xml) } -> let results = to_ltacprof_results xml in let other_results = (* Multi success can cause this *) try SM.find s !data diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index f30f8a9438..3655df8951 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -95,7 +95,6 @@ let rec make_form atom_env gls term = let normalize=special_nf gls in let cciterm=special_whd gls term in let sigma = Tacmach.project gls in - let inj = EConstr.Unsafe.to_constr in match EConstr.kind sigma cciterm with Prod(_,a,b) -> if noccurn sigma 1 b && |