diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:36:50 +0100 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-12-18 09:36:50 +0100 |
| commit | 0168ee0b6463a9ef44d768b0020b34785986c1cb (patch) | |
| tree | c3bb1d2eef4fa5edfd2d431669015db896e08633 /plugins/funind/indfun.ml | |
| parent | 50bd89748af03bb28ad7024f2ceef500489a91b0 (diff) | |
| parent | 53f5cc210da4debd5264d6d8651a76281b0b4256 (diff) | |
Merge PR #6413: [econstr] Switch constrintern API to non-imperative style.
Diffstat (limited to 'plugins/funind/indfun.ml')
| -rw-r--r-- | plugins/funind/indfun.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml index 9e22ad306..357755e46 100644 --- a/plugins/funind/indfun.ml +++ b/plugins/funind/indfun.ml @@ -158,8 +158,8 @@ let build_newrecursive (fun (env,impls) (((_,recname),_),bl,arityc,_) -> let arityc = Constrexpr_ops.mkCProdN 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 + let evd = Evd.from_env env0 in + let evd, (_, (_, impls')) = Constrintern.interp_context_evars env evd bl in let impl = Constrintern.compute_internalization_data env0 Constrintern.Recursive arity impls' in let open Context.Named.Declaration in (Environ.push_named (LocalAssum (recname,arity)) env, Id.Map.add recname impl impls)) |