diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
| -rw-r--r-- | plugins/subtac/subtac_classes.ml | 4 | ||||
| -rw-r--r-- | plugins/subtac/subtac_command.ml | 18 |
4 files changed, 14 insertions, 14 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index e571803273..38492f88b5 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -152,8 +152,8 @@ let build_newrecursive let arityc = Topconstr.prod_constr_expr arityc bl in let arity = Constrintern.interp_type sigma env0 arityc in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity [] in - (Environ.push_named (recname,None,arity) env, (recname, impl) :: impls)) - (env0,[]) lnameargsardef in + (Environ.push_named (recname,None,arity) env, Idmap.add recname impl impls)) + (env0,Constrintern.empty_internalization_env) lnameargsardef in let recdef = (* Declare local notations *) let fs = States.freeze() in diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index feff5d67c6..4217b83faf 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1410,7 +1410,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num let equation_id = add_suffix function_name "_equation" in let functional_id = add_suffix function_name "_F" in let term_id = add_suffix function_name "_terminate" in - let functional_ref = declare_fun functional_id (IsDefinition Definition) res in + let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) res in let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> (x,None,t)) pre_rec_args) env in let relation = interp_constr diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml index aae5383892..640d3e60d6 100644 --- a/plugins/subtac/subtac_classes.ml +++ b/plugins/subtac/subtac_classes.ml @@ -26,11 +26,11 @@ open Util module SPretyping = Subtac_pretyping.Pretyping -let interp_constr_evars_gen evdref env ?(impls=[]) kind c = +let interp_constr_evars_gen evdref env ?(impls=Constrintern.empty_internalization_env) kind c = SPretyping.understand_tcc_evars evdref env kind (intern_gen (kind=IsType) ~impls !evdref env c) -let interp_casted_constr_evars evdref env ?(impls=[]) c typ = +let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internalization_env) c typ = interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c let interp_context_evars evdref env params = diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml index 9098922e31..6fe31646ba 100644 --- a/plugins/subtac/subtac_command.ml +++ b/plugins/subtac/subtac_command.ml @@ -52,7 +52,7 @@ let evar_nf isevars c = Evarutil.nf_evar !isevars c let interp_gen kind isevars env - ?(impls=[]) ?(allow_patvar=false) ?(ltacvars=([],[])) + ?(impls=Constrintern.empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=([],[])) c = let c' = Constrintern.intern_gen (kind=IsType) ~impls ~allow_patvar ~ltacvars ( !isevars) env c in let c' = SPretyping.understand_tcc_evars isevars env kind c' in @@ -61,13 +61,13 @@ let interp_gen kind isevars env let interp_constr isevars env c = interp_gen (OfType None) isevars env c -let interp_type_evars isevars env ?(impls=[]) c = +let interp_type_evars isevars env ?(impls=Constrintern.empty_internalization_env) c = interp_gen IsType isevars env ~impls c -let interp_casted_constr isevars env ?(impls=[]) c typ = +let interp_casted_constr isevars env ?(impls=Constrintern.empty_internalization_env) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c -let interp_casted_constr_evars isevars env ?(impls=[]) c typ = +let interp_casted_constr_evars isevars env ?(impls=Constrintern.empty_internalization_env) c typ = interp_gen (OfType (Some typ)) isevars env ~impls c let interp_open_constr isevars env c = @@ -300,11 +300,11 @@ let build_wellfounded (recname,n,bl,arityc,body) r measure notation = Constrintern.compute_internalization_data env Constrintern.Recursive full_arity impls in - let newimpls = [(recname, (r, l, impls @ - [Some (id_of_string "recproof", Impargs.Manual, (true, false))], - scopes @ [None]))] in - interp_casted_constr isevars ~impls:newimpls - (push_rel_context ctx env) body (lift 1 top_arity) + let newimpls = Idmap.singleton recname + (r, l, impls @ [(Some (id_of_string "recproof", Impargs.Manual, (true, false)))], + scopes @ [None]) in + interp_casted_constr isevars ~impls:newimpls + (push_rel_context ctx env) body (lift 1 top_arity) in let intern_body_lam = it_mkLambda_or_LetIn intern_body (curry_fun :: lift_lets @ fun_bl) in let prop = mkLambda (Name argname, argtyp, top_arity_let) in |