diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/indfun.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/subtac_command.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 79ef009729..027aae7a79 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -168,7 +168,7 @@ let build_newrecursive if Impargs.is_implicit_args() then Impargs.compute_implicits env0 arity else [] in - let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in + let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in (Environ.push_named (recname,None,arity) env, impls')) (env0,[]) lnameargsardef in let recdef = diff --git a/contrib/subtac/subtac_command.ml b/contrib/subtac/subtac_command.ml index 503f346193..1914002124 100644 --- a/contrib/subtac/subtac_command.ml +++ b/contrib/subtac/subtac_command.ml @@ -385,7 +385,7 @@ let interp_recursive fixkind l boxed = let env_rec = push_named_context rec_sign env in (* Get interpretation metadatas *) - let impls = Command.compute_interning_datas env [] fixnames fixtypes fiximps in + let impls = Command.compute_interning_datas env Constrintern.Recursive [] fixnames fixtypes fiximps in let notations = List.fold_right Option.List.cons ntnl [] in (* Interp bodies with rollback because temp use of notations/implicit *) |