diff options
| author | Hugo Herbelin | 2016-12-05 11:36:12 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-03-23 22:13:56 +0100 |
| commit | 8f5d447769a41cd251701272a6ff71a7a20de658 (patch) | |
| tree | 8146cf9cdfc399f43e2ecd9bd9df49dfae49b635 /plugins | |
| parent | 80d36bc6538b7feaab3dfa43f6e234ae85b55692 (diff) | |
Improving the API of constrexpr_ops.mli.
Deprecating abstract_constr_expr in favor of mkCLambdaN,
prod_constr_expr in favor of mkCProdN.
Note: They did not do exactly the same, the first ones were
interpreting "(x y z:_)" as "(x:_) (y:_) (z:_)" while the second ones
were preserving the original sharing of the type, what I think is the
correct thing to do.
So, there is also a "fix" of semantic here.
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 99b04898ba..94b6b912d3 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -151,7 +151,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 @@ -436,7 +436,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 @@ -467,7 +467,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 |