From 62fa31d219dcf2129c55b3c46b8cc25be60edcab Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 10:18:10 +0200 Subject: Program: remove debug tracing --- toplevel/obligations.ml | 6 ------ 1 file changed, 6 deletions(-) (limited to 'toplevel') diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index a18552c5e..6f7a5f684 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -24,10 +24,6 @@ open Util let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false) let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false) -let trace s = - if !Flags.debug then msg_debug s - else () - let succfix (depth, fixrels) = (succ depth, List.map succ fixrels) @@ -871,8 +867,6 @@ let rec solve_obligation prg num tac = let auto n tac oblset = auto_solve_obligations n ~oblset tac in let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type hook in - let () = trace (str "Started obligation " ++ int user_num ++ str " proof: " ++ - Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in let _ = Pfedit.by (snd (get_default_tactic ())) in Option.iter (fun tac -> Pfedit.set_end_tac tac) tac -- cgit v1.2.3 From 4ae315f92e4a9849a56d3d9b0da33027f362d6e8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 26 May 2016 10:55:15 +0200 Subject: 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. --- plugins/funind/recdef.ml | 10 +++++----- test-suite/bugs/closed/4725.v | 38 ++++++++++++++++++++++++++++++++++++++ toplevel/command.ml | 1 - 3 files changed, 43 insertions(+), 6 deletions(-) create mode 100644 test-suite/bugs/closed/4725.v (limited to 'toplevel') 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 *) diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v new file mode 100644 index 000000000..fd5e0fb60 --- /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 8f7c38997..8eb2232ed 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 () = -- cgit v1.2.3 From c064fb933a16dc25b8172a1a2e758f538ee7285e Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 18 Jun 2016 11:18:01 +0200 Subject: A hack to fix another regression with Ltac trace report in 8.5. E.g. Goal 0=0 -> true=true. intro H; rewrite H1. was highlighting H1 but Goal 0=0 -> true=true. intro H; rewrite H. was only highlighting the whole "intro H; rewrite H". --- toplevel/himsg.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) (limited to 'toplevel') diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 244174f65..13a6489b9 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1307,12 +1307,17 @@ let extract_ltac_trace trace eloc = else (* We entered a primitive tactic, we don't display trace but report on the finest location *) + let finer_loc loc1 loc2 = Loc.merge loc1 loc2 = loc2 in let best_loc = - if not (Loc.is_ghost eloc) then eloc else - (* trace is with innermost call coming first *) - let rec aux = function - | (loc,_)::tail when not (Loc.is_ghost loc) -> loc - | _::tail -> aux tail - | [] -> Loc.ghost in - aux trace in + (* trace is with innermost call coming first *) + let rec aux best_loc = function + | (loc,_)::tail -> + if Loc.is_ghost best_loc || + not (Loc.is_ghost loc) && finer_loc loc best_loc + then + aux loc tail + else + aux best_loc tail + | [] -> best_loc in + aux eloc trace in None, best_loc -- cgit v1.2.3