diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-26 10:55:15 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2016-05-26 11:01:28 +0200 |
| commit | 4ae315f92e4a9849a56d3d9b0da33027f362d6e8 (patch) | |
| tree | f1a41706cd8de59b5ce215ff66f8107299fc791f /plugins/funind | |
| parent | 62fa31d219dcf2129c55b3c46b8cc25be60edcab (diff) | |
Univs/Program/Function: Fix bug #4725
- In Program, a check_evars_are_solved was introduced
too early. Program does it's checking of evars by itself.
- In Function, the universe environments were not threaded
correctly.
Diffstat (limited to 'plugins/funind')
| -rw-r--r-- | plugins/funind/recdef.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 065d0fe53..bc8e721ed 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1510,13 +1510,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num 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 Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in + (* Refresh the global universes, now including those of _F *) + let evm = Evd.from_env (Global.env ()) 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 = - fst (*FIXME*)(interp_constr - env_with_pre_rec_args - (Evd.from_env env_with_pre_rec_args) - r) + let relation, evuctx = + interp_constr env_with_pre_rec_args evm r in + let evm = Evd.from_ctx evuctx in let tcc_lemma_name = add_suffix function_name "_tcc" in let tcc_lemma_constr = ref None in (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *) |