diff options
| -rw-r--r-- | plugins/funind/recdef.ml | 10 | ||||
| -rw-r--r-- | test-suite/bugs/closed/4725.v | 38 | ||||
| -rw-r--r-- | toplevel/command.ml | 1 |
3 files changed, 43 insertions, 6 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 065d0fe537..bc8e721edc 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 *) diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v new file mode 100644 index 0000000000..fd5e0fb60d --- /dev/null +++ b/test-suite/bugs/closed/4725.v @@ -0,0 +1,38 @@ +Require Import EquivDec Equivalence List Program. +Require Import Relation_Definitions. +Import ListNotations. +Generalizable All Variables. + +Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V +:= + match l with + | nil => nil + | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl) + end. + +Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (xs : list V) (x : V) : + length (removeV x xs) < length (x :: xs). + Proof. Admitted. + +(* Function version *) +Set Printing Universes. + +Require Import Recdef. + +Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV : +@EqDec V eqV equivV} (l : list V) { measure length l} := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) + end. +Proof. intros. apply remove_le. Qed. + +(* Program version *) + +Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V) + { measure (@length V l) lt } := + match l with + | nil => nil + | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _ + end. diff --git a/toplevel/command.ml b/toplevel/command.ml index 8f7c389975..8eb2232eda 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -923,7 +923,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation = let binders = letbinders @ [arg] in let binders_env = push_rel_context binders_rel env in let rel, _ = interp_constr_evars_impls env evdref r in - let () = check_evars_are_solved env !evdref (Evd.empty,!evdref) in let relty = Typing.unsafe_type_of env !evdref rel in let relargty = let error () = |