From d8825650bd2b7855a92195c032a539aa3f09c9ef Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 8 Jun 2016 17:33:12 -0400 Subject: Unbreak singleton list-like notation (-compat 8.4) With this commit, it is possible to write notations so that singleton lists are usable in both 8.4 and 8.5pl1 -compat. Longer lists await the ability to remove notations from the parser. --- test-suite/bugs/closed/4684.v | 32 ++++++++++++++++++++++++++ test-suite/bugs/closed/4733.v | 52 +++++++++++++++++++++++++++++++++++++++++++ test-suite/bugs/opened/4803.v | 34 ++++++++++++++++++++++++++++ theories/Compat/Coq84.v | 24 ++++++++++++++++++++ 4 files changed, 142 insertions(+) create mode 100644 test-suite/bugs/closed/4684.v create mode 100644 test-suite/bugs/closed/4733.v create mode 100644 test-suite/bugs/opened/4803.v diff --git a/test-suite/bugs/closed/4684.v b/test-suite/bugs/closed/4684.v new file mode 100644 index 000000000..9c0bed42c --- /dev/null +++ b/test-suite/bugs/closed/4684.v @@ -0,0 +1,32 @@ +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. + +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/closed/4733.v b/test-suite/bugs/closed/4733.v new file mode 100644 index 000000000..ac0653492 --- /dev/null +++ b/test-suite/bugs/closed/4733.v @@ -0,0 +1,52 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. + +(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) + +Notation " [ x ; y ; .. ; z ] " := (mycons x (mycons y .. (mycons z mynil) ..)) : mylist_scope. +(* Now these all work, but not so in 8.4. If we get the ability to remove notations, and the above fails can be removed, this section can also just be removed. *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ]%mylist : mylist _. +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. diff --git a/test-suite/bugs/opened/4803.v b/test-suite/bugs/opened/4803.v new file mode 100644 index 000000000..3ca5c095f --- /dev/null +++ b/test-suite/bugs/opened/4803.v @@ -0,0 +1,34 @@ +(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *) +(*Suppose a user wants to declare a new list-like notation with support for singletons in both 8.4 and 8.5. If they use*) +Require Import Coq.Lists.List. +Require Import Coq.Vectors.Vector. +Import ListNotations. +Import VectorNotations. +Set Implicit Arguments. +Inductive mylist T := mynil | mycons (_ : T) (_ : mylist T). +Arguments mynil {_}, _. + +Delimit Scope mylist_scope with mylist. +Bind Scope mylist_scope with mylist. +Delimit Scope vector_scope with vector. + +Notation " [ ] " := mynil (format "[ ]") : mylist_scope. +Notation " [ x ] " := (mycons x mynil) : mylist_scope. +Notation " [ x ; .. ; y ] " := (mycons x .. (mycons y mynil) ..) : mylist_scope. + +(** All of these should work fine in -compat 8.4 mode, just as they do in Coq 8.4. There needs to be a way to specify notations above so that all of these [Check]s go through in both 8.4 and 8.5 *) +Check [ ]%mylist : mylist _. +Check [ ]%list : list _. +Check []%vector : Vector.t _ _. +Check [ _ ]%mylist : mylist _. +Check [ _ ]%list : list _. +Check [ _ ]%vector : Vector.t _ _. +Check [ _ ; _ ]%list : list _. +Check [ _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser; it should be added to Compat/Coq84.v *) +Check [ _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) +Check [ _ ; _ ; _ ; _ ]%list : list _. +Check [ _ ; _ ; _ ; _ ]%vector : Vector.t _ _. +Fail Check [ _ ; _ ; _ ; _ ]%mylist : mylist _. (* ideally, this should work, but that requires removing notations from the parser *) diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index aa4411704..574f283f1 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -66,3 +66,27 @@ Coercion sigT_of_sig : sig >-> sigT. Coercion sig_of_sigT : sigT >-> sig. Coercion sigT2_of_sig2 : sig2 >-> sigT2. Coercion sig2_of_sigT2 : sigT2 >-> sig2. + +(** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5. This is necessary. These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *) +Require Coq.Lists.List. +Require Coq.Vectors.VectorDef. +Module Export Coq. +Module Export Lists. +Module List. +Module ListNotations. +Include Coq.Lists.List.ListNotations. +Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. +End ListNotations. +End List. +End Lists. +Module Export Vectors. +Module VectorDef. +Module VectorNotations. +Import Coq.Vectors.VectorDef.VectorNotations. +Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. +End VectorNotations. +End VectorDef. +End Vectors. +End Coq. +Export Vectors.VectorDef.VectorNotations. +Export List.ListNotations. -- cgit v1.2.3 From a5b631f7260e7d29defd8bd5c67db543742c9ecd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 9 May 2016 17:40:04 +0200 Subject: congruence/univs: properly refresh (fix #4609) In congruence, refresh universes including the Set/Prop ones so that congruence works with cumulativity, not restricting itself to the inferred types of terms that are manipulated but allowing them to be used at more general types. This fixes bug #4609. --- plugins/cc/cctac.ml | 109 ++++++++++++++++++++-------------------- pretyping/evarsolve.ml | 7 ++- pretyping/evarsolve.mli | 8 ++- test-suite/bugs/closed/4069.v | 39 ++++++++++++++ test-suite/success/congruence.v | 21 ++++++++ 5 files changed, 127 insertions(+), 57 deletions(-) create mode 100644 test-suite/success/congruence.v diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index df4a7319a..de555f0a7 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -245,10 +245,10 @@ let build_projection intype outtype (cstr:pconstructor) special default gls= let _M =mkMeta -let app_global f args k = +let app_global f args k = Tacticals.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) -let new_app_global f args k = +let new_app_global f args k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> k (mkApp (fc, args))) let new_refine c = Proofview.V82.tactic (refine c) @@ -258,7 +258,19 @@ let assert_before n c = let evm, _ = Tacmach.New.pf_apply type_of gl c in Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (assert_before n c) end - + +let refresh_type env evm ty = + Evarsolve.refresh_universes ~status:Evd.univ_flexible ~propset:true + (Some false) env evm ty + +let refresh_universes ty k = + Proofview.Goal.enter begin fun gl -> + let env = Proofview.Goal.env gl in + let evm = Proofview.Goal.sigma gl in + let evm, ty = refresh_type env evm ty in + Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k ty) + end + let rec proof_tac p : unit Proofview.tactic = Proofview.Goal.nf_enter begin fun gl -> let type_of t = Tacmach.New.pf_unsafe_type_of gl t in @@ -268,35 +280,31 @@ let rec proof_tac p : unit Proofview.tactic = | SymAx c -> let l=constr_of_term p.p_lhs and r=constr_of_term p.p_rhs in - let typ = (* Termops.refresh_universes *) type_of l in - new_app_global _sym_eq [|typ;r;l;c|] exact_check + refresh_universes (type_of l) (fun typ -> + new_app_global _sym_eq [|typ;r;l;c|] exact_check) | Refl t -> let lr = constr_of_term t in - let typ = (* Termops.refresh_universes *) type_of lr in - new_app_global _refl_equal [|typ;constr_of_term t|] exact_check + refresh_universes (type_of lr) (fun typ -> + new_app_global _refl_equal [|typ;constr_of_term t|] exact_check) | Trans (p1,p2)-> let t1 = constr_of_term p1.p_lhs and t2 = constr_of_term p1.p_rhs and t3 = constr_of_term p2.p_rhs in - let typ = (* Termops.refresh_universes *) (type_of t2) in + refresh_universes (type_of t2) (fun typ -> let prf = new_app_global _trans_eq [|typ;t1;t2;t3;_M 1;_M 2|] in - Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)] + Tacticals.New.tclTHENS (prf new_refine) [(proof_tac p1);(proof_tac p2)]) | Congr (p1,p2)-> let tf1=constr_of_term p1.p_lhs and tx1=constr_of_term p2.p_lhs and tf2=constr_of_term p1.p_rhs and tx2=constr_of_term p2.p_rhs in - let typf = (* Termops.refresh_universes *)(type_of tf1) in - let typx = (* Termops.refresh_universes *) (type_of tx1) in - let typfx = (* Termops.refresh_universes *) (type_of (mkApp (tf1,[|tx1|]))) in + refresh_universes (type_of tf1) (fun typf -> + refresh_universes (type_of tx1) (fun typx -> + refresh_universes (type_of (mkApp (tf1,[|tx1|]))) (fun typfx -> let id = Tacmach.New.of_old (fun gls -> pf_get_new_id (Id.of_string "f") gls) gl in let appx1 = mkLambda(Name id,typf,mkApp(mkRel 1,[|tx1|])) in - let lemma1 = - app_global _f_equal - [|typf;typfx;appx1;tf1;tf2;_M 1|] in - let lemma2= - app_global _f_equal - [|typx;typfx;tf2;tx1;tx2;_M 1|] in + let lemma1 = app_global _f_equal [|typf;typfx;appx1;tf1;tf2;_M 1|] in + let lemma2 = app_global _f_equal [|typx;typfx;tf2;tx1;tx2;_M 1|] in let prf = app_global _trans_eq [|typfx; @@ -310,53 +318,51 @@ let rec proof_tac p : unit Proofview.tactic = reflexivity; Tacticals.New.tclZEROMSG (Pp.str - "I don't know how to handle dependent equality")]] + "I don't know how to handle dependent equality")]]))) | Inject (prf,cstr,nargs,argind) -> let ti=constr_of_term prf.p_lhs in let tj=constr_of_term prf.p_rhs in let default=constr_of_term p.p_lhs in - let intype = (* Termops.refresh_universes *) (type_of ti) in - let outtype = (* Termops.refresh_universes *) (type_of default) in let special=mkRel (1+nargs-argind) in - let proj = + refresh_universes (type_of ti) (fun intype -> + refresh_universes (type_of default) (fun outtype -> + let proj = Tacmach.New.of_old (build_projection intype outtype cstr special default) gl in let injt= app_global _f_equal [|intype;outtype;proj;ti;tj;_M 1|] in - Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf) + Tacticals.New.tclTHEN (Proofview.V82.tactic (injt refine)) (proof_tac prf))) with e when Proofview.V82.catchable_exception e -> Proofview.tclZERO e end let refute_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt1)) gl - in - let neweq= new_app_global _eq [|intype;tt1;tt2|] in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let false_t=mkApp (c,[|mkVar hid|]) in + let k intype = + let neweq= new_app_global _eq [|intype;tt1;tt2|] in Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) [proof_tac p; simplest_elim false_t] + in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt1) k end let refine_exact_check c gl = let evm, _ = pf_apply type_of gl c in Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl -let convert_to_goal_tac c t1 t2 p = +let convert_to_goal_tac c t1 t2 p = Proofview.Goal.nf_enter begin fun gl -> let tt1=constr_of_term t1 and tt2=constr_of_term t2 in - let sort = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls tt2)) gl - in - let neweq= new_app_global _eq [|sort;tt1;tt2|] in - let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in - let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in - let identity=mkLambda (Name x,sort,mkRel 1) in - let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in + let k sort = + let neweq= new_app_global _eq [|sort;tt1;tt2|] in + let e = Tacmach.New.of_old (pf_get_new_id (Id.of_string "e")) gl in + let x = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in + let identity=mkLambda (Name x,sort,mkRel 1) in + let endt=app_global _eq_rect [|sort;tt1;identity;c;tt2;mkVar e|] in Tacticals.New.tclTHENS (neweq (assert_before (Name e))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)] + in refresh_universes (Tacmach.New.pf_unsafe_type_of gl tt2) k end let convert_to_hyp_tac c1 t1 c2 t2 p = @@ -372,33 +378,28 @@ let convert_to_hyp_tac c1 t1 c2 t2 p = let discriminate_tac (cstr,u as cstru) p = Proofview.Goal.nf_enter begin fun gl -> let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in - let intype = - Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_unsafe_type_of gls t1)) gl - in + let env = Proofview.Goal.env gl in let concl = Proofview.Goal.concl gl in - (* let evm,outsort = Evd.new_sort_variable Evd.univ_rigid (project gls) in *) - (* let outsort = mkSort outsort in *) let xid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "X")) gl in - (* let tid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "t")) gl in *) - (* let identity=mkLambda(Name xid,outsort,mkLambda(Name tid,mkRel 1,mkRel 1)) in *) let identity = Universes.constr_of_global (Lazy.force _I) in - (* let trivial=pf_unsafe_type_of gls identity in *) let trivial = Universes.constr_of_global (Lazy.force _True) in - let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in + let evm = Proofview.Goal.sigma gl in + let evm, intype = refresh_type env evm (Tacmach.New.pf_unsafe_type_of gl t1) in + let evm, outtype = Evd.new_sort_variable Evd.univ_flexible evm in let outtype = mkSort outtype in - let pred=mkLambda(Name xid,outtype,mkRel 1) in + let pred = mkLambda(Name xid,outtype,mkRel 1) in let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in let proj = Tacmach.New.of_old (build_projection intype outtype cstru trivial concl) gl in let injt=app_global _f_equal - [|intype;outtype;proj;t1;t2;mkVar hid|] in + [|intype;outtype;proj;t1;t2;mkVar hid|] in let endt k = injt (fun injt -> - app_global _eq_rect - [|outtype;trivial;pred;identity;concl;injt|] k) in + app_global _eq_rect + [|outtype;trivial;pred;identity;concl;injt|] k) in let neweq=new_app_global _eq [|intype;t1;t2|] in Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS evm) - (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) - [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) + (Tacticals.New.tclTHENS (neweq (assert_before (Name hid))) + [proof_tac p; Proofview.V82.tactic (endt refine_exact_check)]) end (* wrap everything *) @@ -482,7 +483,7 @@ let congruence_tac depth l = This isn't particularly related with congruence, apart from the fact that congruence is called internally. *) - + let mk_eq f c1 c2 k = Tacticals.New.pf_constr_of_global (Lazy.force f) (fun fc -> Proofview.Goal.enter begin @@ -495,7 +496,7 @@ let mk_eq f c1 c2 k = Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS evm)) (k term) end) - + let f_equal = Proofview.Goal.nf_enter begin fun gl -> let concl = Proofview.Goal.concl gl in diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 29af199a1..c2d47790d 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,8 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false) + pbty env evd t = let evdref = ref evd in let modified = ref false in let rec refresh status dir t = @@ -62,6 +63,10 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) pbty env evd t = else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' + | Sort (Prop _ as s) when propset && not dir -> + let s' = evd_comb0 (new_sort_variable status) evdref in + let evd = set_leq_sort env !evdref s s' in + modified := true; evdref := evd; mkSort s' | Prod (na,u,v) -> mkProd (na,u,refresh status dir v) | _ -> t diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 918ba12f0..9ee815ebc 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -34,8 +34,12 @@ type conv_fun_bool = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> bool option -> existential -> constr -> evar_map -val refresh_universes : ?status:Evd.rigid -> - ?onlyalg:bool (* Only algebraic universes *) -> +val refresh_universes : + ?status:Evd.rigid -> + ?onlyalg:bool (* Only algebraic universes *) -> + ?propset:bool -> + (* Also refresh Prop and Set universes, so that the returned type can be any supertype + of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> env -> evar_map -> types -> evar_map * types diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 21b03ce54..11289f757 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -49,3 +49,42 @@ Lemma bar {A} n m (x : A) : skipn n (replicate m x) = replicate (m - n) x. Proof. intros. f_equal. (* 8.5: one goal, n = m - n *) +Abort. + +Variable F : nat -> Set. +Variable X : forall n, F (n + 1). + +Definition sequator{X Y: Set}{eq:X=Y}(x:X) : Y := eq_rec _ _ x _ eq. +Definition tequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq. +Polymorphic Definition pequator{X Y}{eq:X=Y}(x:X) : Y := eq_rect _ _ x _ eq. + +Goal {n:nat & F (S n)}. +eexists. +unshelve eapply (sequator (X _)). +f_equal. (*behaves*) +Undo 2. +unshelve eapply (pequator (X _)). +f_equal. (*behaves*) +Undo 2. +unshelve eapply (tequator (X _)). +f_equal. (*behaves now *) +Focus 2. exact 0. +simpl. +reflexivity. +Defined. + +(* Part 2: modulo casts introduced by refine due to reductions in goals *) + +Goal {n:nat & F (S n)}. +eexists. +(*misbehaves, although same goal as above*) +Set Printing All. +unshelve refine (sequator (X _)); revgoals. +2:exact 0. reflexivity. +Undo 3. +unshelve refine (pequator (X _)); revgoals. +f_equal. +Undo 2. +unshelve refine (tequator (X _)); revgoals. +f_equal. +Admitted. \ No newline at end of file diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v new file mode 100644 index 000000000..873d2f9f7 --- /dev/null +++ b/test-suite/success/congruence.v @@ -0,0 +1,21 @@ +(* Example by Jonathan Leivant, congruence and tauto up to universes *) +Variables S1 S2 : Set. + +Goal @eq Type S1 S2 -> @eq Type S1 S2. +intro H. +tauto. +Qed. + +Definition T1 : Type := S1. +Definition T2 : Type := S2. + +Goal T1 = T1. +congruence. +Undo. +tauto. +Undo. +unfold T1. +congruence. +Undo. +tauto. +Qed. -- cgit v1.2.3 From ee8009e05d3e782ee6333d0054ee2fce5cda89a4 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 9 May 2016 17:43:59 +0200 Subject: congruence: remove casts of indexed terms This fixes the end of bug #4069, provoked by a use of unshelve refine which introduces a cast. --- plugins/cc/cctac.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index de555f0a7..ba34d49bb 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -80,8 +80,10 @@ let rec decompose_term env sigma t= | Proj (p, c) -> let canon_const kn = constant_of_kn (canonical_con kn) in let p' = Projection.map canon_const p in - (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) - | _ ->if closed0 t then (Symb t) else raise Not_found + (Appli (Symb (mkConst (Projection.constant p')), decompose_term env sigma c)) + | _ -> + let t = strip_outer_cast t in + if closed0 t then Symb t else raise Not_found (* decompose equality in members and type *) open Globnames -- cgit v1.2.3 From 71d4c435e42c24c21ae43f0ddcc7a71bee1009f5 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 9 May 2016 18:31:01 +0200 Subject: congruence: Restrict refreshing to Set Because refreshing Prop is not semantics-preserving, the new universe is >= Set, so cannot be minimized to Prop afterwards. --- kernel/univ.ml | 2 +- plugins/cc/cctac.ml | 2 +- pretyping/evarsolve.ml | 4 ++-- pretyping/evarsolve.mli | 2 +- test-suite/success/cc.v | 14 ++++++++++++++ test-suite/success/congruence.v | 21 --------------------- 6 files changed, 19 insertions(+), 26 deletions(-) delete mode 100644 test-suite/success/congruence.v diff --git a/kernel/univ.ml b/kernel/univ.ml index 117bc4e5f..2cc57c38c 100644 --- a/kernel/univ.ml +++ b/kernel/univ.ml @@ -754,7 +754,7 @@ let is_set_arc u = Level.is_set u.univ let is_prop_arc u = Level.is_prop u.univ exception AlreadyDeclared - + let add_universe vlev strict g = try let _arcv = UMap.find vlev g in diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index ba34d49bb..c8d857b31 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -262,7 +262,7 @@ let assert_before n c = end let refresh_type env evm ty = - Evarsolve.refresh_universes ~status:Evd.univ_flexible ~propset:true + Evarsolve.refresh_universes ~status:Evd.univ_flexible ~refreshset:true (Some false) env evm ty let refresh_universes ty k = diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index c2d47790d..0db309f94 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -47,7 +47,7 @@ let refresh_level evd s = | None -> true | Some l -> not (Evd.is_flexible_level evd l) -let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false) +let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false) pbty env evd t = let evdref = ref evd in let modified = ref false in @@ -63,7 +63,7 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(propset=false) else set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' - | Sort (Prop _ as s) when propset && not dir -> + | Sort (Prop Pos as s) when refreshset && not dir -> let s' = evd_comb0 (new_sort_variable status) evdref in let evd = set_leq_sort env !evdref s s' in modified := true; evdref := evd; mkSort s' diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli index 9ee815ebc..f94c83b6d 100644 --- a/pretyping/evarsolve.mli +++ b/pretyping/evarsolve.mli @@ -37,7 +37,7 @@ val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> val refresh_universes : ?status:Evd.rigid -> ?onlyalg:bool (* Only algebraic universes *) -> - ?propset:bool -> + ?refreshset:bool -> (* Also refresh Prop and Set universes, so that the returned type can be any supertype of the original type *) bool option (* direction: true for levels lower than the existing levels *) -> diff --git a/test-suite/success/cc.v b/test-suite/success/cc.v index a70d91963..0b0e93eb5 100644 --- a/test-suite/success/cc.v +++ b/test-suite/success/cc.v @@ -131,3 +131,17 @@ End bug_2447. +(* Example by Jonathan Leivant, congruence up to universes *) +Section JLeivant. + Variables S1 S2 : Set. + + Definition T1 : Type := S1. + Definition T2 : Type := S2. + + Goal T1 = T1. + congruence. + Undo. + unfold T1. + congruence. + Qed. +End JLeivant. diff --git a/test-suite/success/congruence.v b/test-suite/success/congruence.v deleted file mode 100644 index 873d2f9f7..000000000 --- a/test-suite/success/congruence.v +++ /dev/null @@ -1,21 +0,0 @@ -(* Example by Jonathan Leivant, congruence and tauto up to universes *) -Variables S1 S2 : Set. - -Goal @eq Type S1 S2 -> @eq Type S1 S2. -intro H. -tauto. -Qed. - -Definition T1 : Type := S1. -Definition T2 : Type := S2. - -Goal T1 = T1. -congruence. -Undo. -tauto. -Undo. -unfold T1. -congruence. -Undo. -tauto. -Qed. -- cgit v1.2.3 From a91bafa58710777506dc30afb1a0e2cc56b941c7 Mon Sep 17 00:00:00 2001 From: thery Date: Tue, 5 Jul 2016 14:02:28 +0200 Subject: Bug fix : variable capture in ltac code of Nsatz changing set (x := val) into let x := fresh "x" in set (x := val) --- plugins/nsatz/Nsatz.v | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/plugins/nsatz/Nsatz.v b/plugins/nsatz/Nsatz.v index 3068b5347..b11d15e5c 100644 --- a/plugins/nsatz/Nsatz.v +++ b/plugins/nsatz/Nsatz.v @@ -298,7 +298,9 @@ Ltac nsatz_call_n info nparam p rr lp kont := match goal with | |- (?c::PEpow _ ?r::?lq0)::?lci0 = _ -> _ => intros _; + let lci := fresh "lci" in set (lci:=lci0); + let lq := fresh "lq" in set (lq:=lq0); kont c rr lq lci end. @@ -380,10 +382,13 @@ Ltac nsatz_generic radicalmax info lparam lvar := end in SplitPolyList ltac:(fun p lp => + let p21 := fresh "p21" in + let lp21 := fresh "lp21" in set (p21:=p) ; set (lp21:=lp); (* idtac "nparam:"; idtac nparam; idtac "p:"; idtac p; idtac "lp:"; idtac lp; *) nsatz_call radicalmax info nparam p lp ltac:(fun c r lq lci => + let q := fresh "q" in set (q := PEmul c (PEpow p21 r)); let Hg := fresh "Hg" in assert (Hg:check lp21 q (lci,lq) = true); -- cgit v1.2.3 From 618dce7fbf7c5b3ed80dacd16be761c4f7487079 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 5 Jul 2016 15:18:44 +0200 Subject: Add mailmap entry. --- .mailmap | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.mailmap b/.mailmap index 13c71558f..c9ca597c7 100644 --- a/.mailmap +++ b/.mailmap @@ -79,7 +79,8 @@ Arnaud Spiwack aspiwack gareuselesinge Enrico Tassi Enrico Tassi Enrico Tassi Enrico Tassi -Laurent Théry thery +Laurent Théry thery +Laurent Théry thery Benjamin Werner werner # Anonymous accounts -- cgit v1.2.3 From 37293bd104434bb15acc7d46b8cba90e70504aac Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Tue, 5 Jul 2016 15:58:20 +0200 Subject: Pass .v files to coqc in Makefile produced by coq_makefile (bug #4896). Coqc now expects physical names for input files, so fix coq_makefile accordingly. --- tools/coq_makefile.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 381e8d08c..617185b8f 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -414,9 +414,9 @@ let implicit () = print "\t$(COQDEP) $(OCAMLLIBS) -c \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; in let v_rules () = - print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $*\n\n"; - print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $*\n\n"; + print "$(VOFILES): %.vo: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; + print "$(GLOBFILES): %.glob: %.v\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) $<\n\n"; + print "$(VFILES:.v=.vio): %.vio: %.v\n\t$(COQC) -quick $(COQDEBUG) $(COQFLAGS) $<\n\n"; print "$(GFILES): %.g: %.v\n\t$(GALLINA) $<\n\n"; print "$(VFILES:.v=.tex): %.tex: %.v\n\t$(COQDOC) $(COQDOCFLAGS) -latex $< -o $@\n\n"; print "$(HTMLFILES): %.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html $< -o $@\n\n"; @@ -424,7 +424,7 @@ in print "$(GHTMLFILES): %.g.html: %.v %.glob\n\t$(COQDOC) $(COQDOCFLAGS) -html -g $< -o $@\n\n"; print "$(addsuffix .d,$(VFILES)): %.v.d: %.v\n"; print "\t$(COQDEP) $(COQLIBS) \"$<\" > \"$@\" || ( RV=$$?; rm -f \"$@\"; exit $${RV} )\n\n"; - print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*\n\n" + print "$(addsuffix .beautified,$(VFILES)): %.v.beautified:\n\t$(COQC) $(COQDEBUG) $(COQFLAGS) -beautify $*.v\n\n" in if !some_mlifile then mli_rules (); if !some_ml4file then ml4_rules (); -- cgit v1.2.3 From 57021d22fabb33b281af4de8f3946cb4424c6422 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 5 Jul 2016 18:28:24 +0200 Subject: congruence fix: test-suite code and update CHANGES This fixes bugs #4069 (not 4609 as mentionned in the git log) and #4718. --- CHANGES | 1 + test-suite/bugs/closed/4069.v | 16 +++++++++++++++- 2 files changed, 16 insertions(+), 1 deletion(-) diff --git a/CHANGES b/CHANGES index 0f5ea97aa..7d5691efe 100644 --- a/CHANGES +++ b/CHANGES @@ -24,6 +24,7 @@ Other bugfixes - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. triggered by CoqIDE +- #4069, #4718: congruence fails when universes are involved. Universes - Disallow silently dropping universe instances applied to variables diff --git a/test-suite/bugs/closed/4069.v b/test-suite/bugs/closed/4069.v index 11289f757..61527764e 100644 --- a/test-suite/bugs/closed/4069.v +++ b/test-suite/bugs/closed/4069.v @@ -87,4 +87,18 @@ f_equal. Undo 2. unshelve refine (tequator (X _)); revgoals. f_equal. -Admitted. \ No newline at end of file +Admitted. + +Goal @eq Set nat nat. +congruence. +Qed. + +Goal @eq Type nat nat. +congruence. +Qed. + +Variable T : Type. + +Goal @eq Type T T. +congruence. +Qed. \ No newline at end of file -- cgit v1.2.3 From 2df88d833767f6a43ac8f08627e1cb9cc0c8b30d Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 5 Jul 2016 17:19:05 +0200 Subject: Prevent unsafe overwriting of Required modules by toplevel library. In coqtop, one could do for instance: Require Import Top. (* Where Top contains a Definition b := true *) Lemma bE : b = true. Proof. reflexivity. Qed. Definition b := false. Lemma bad : False. Proof. generalize bE; compute; discriminate. Qed. That proof could however not be saved because of the circular dependency check. Safe_typing now checks that we are not requiring (Safe_typing.import) a library with the same logical name as the current one. --- kernel/safe_typing.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 62753962c..927278965 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -859,6 +859,9 @@ let export ?except senv dir = let import lib cst vodigest senv = check_required senv.required lib.comp_deps; check_engagement senv.env lib.comp_enga; + if DirPath.equal (ModPath.dp senv.modpath) lib.comp_name then + Errors.errorlabstrm "Safe_typing.import" + (Pp.strbrk "Cannot load a library with the same name as the current one."); let mp = MPfile lib.comp_name in let mb = lib.comp_mod in let env = Environ.push_context_set ~strict:true -- cgit v1.2.3 From f6701cffa04c0df25634ad60004fbfcf4ca422ec Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 5 Jul 2016 14:05:07 -0400 Subject: Compat84: Don't mess with stdlib modules We don't actually need to, unless we want to support the (presumably uncommon) use-case of someone using [Import VectorNotations] to override their local notation for things in vector_scope. Additionally, we now maintain the behavior that [Import VectorNotations] opens vector_scope. --- theories/Compat/Coq84.v | 18 ------------------ 1 file changed, 18 deletions(-) diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v index 574f283f1..c157c5e85 100644 --- a/theories/Compat/Coq84.v +++ b/theories/Compat/Coq84.v @@ -70,23 +70,5 @@ Coercion sig2_of_sigT2 : sigT2 >-> sig2. (** As per bug #4733 (https://coq.inria.fr/bugs/show_bug.cgi?id=4733), we want the user to be able to create custom list-like notatoins that work in both 8.4 and 8.5. This is necessary. These should become compat 8.4 notations in the relevant files, but these modify the parser (bug #4798), so this cannot happen until that bug is fixed. *) Require Coq.Lists.List. Require Coq.Vectors.VectorDef. -Module Export Coq. -Module Export Lists. -Module List. -Module ListNotations. -Include Coq.Lists.List.ListNotations. Notation " [ x ; .. ; y ] " := (cons x .. (cons y nil) ..) : list_scope. -End ListNotations. -End List. -End Lists. -Module Export Vectors. -Module VectorDef. -Module VectorNotations. -Import Coq.Vectors.VectorDef.VectorNotations. Notation " [ x ; .. ; y ] " := (VectorDef.cons _ x _ .. (VectorDef.cons _ y _ (nil _)) ..) : vector_scope. -End VectorNotations. -End VectorDef. -End Vectors. -End Coq. -Export Vectors.VectorDef.VectorNotations. -Export List.ListNotations. -- cgit v1.2.3 From 0094b2aa93feda2329fdec0131cffc9ea9114f41 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 5 Jul 2016 15:22:03 -0700 Subject: Restore option_map in FMapFacts This definition was removed by a4043608f704f026de7eb5167a109ca48e00c221 (This commit adds full universe polymorphism and fast projections to Coq), for reasons I do not know. This means that things like `unfold option_map` work only in 8.5, while `unfold .option_map` works only in 8.4. This allows `unfold` to work correctly in both 8.4 and 8.5. --- theories/FSets/FMapFacts.v | 2 ++ 1 file changed, 2 insertions(+) diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index eaeb2914b..741ee69d3 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -437,6 +437,8 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed. +Notation option_map := option_map (compat "8.4"). + Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = option_map f (find x m). Proof. -- cgit v1.2.3 From 2d449a9db34d1cfaff3b698cfc5b435e00100461 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 5 Jul 2016 16:01:04 -0700 Subject: Move option_map notation up This way, it's not eaten by a section --- theories/FSets/FMapFacts.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/theories/FSets/FMapFacts.v b/theories/FSets/FMapFacts.v index 741ee69d3..67bb56448 100644 --- a/theories/FSets/FMapFacts.v +++ b/theories/FSets/FMapFacts.v @@ -24,6 +24,8 @@ Hint Extern 1 (Equivalence _) => constructor; congruence. Module WFacts_fun (E:DecidableType)(Import M:WSfun E). +Notation option_map := option_map (compat "8.4"). + Notation eq_dec := E.eq_dec. Definition eqb x y := if eq_dec x y then true else false. @@ -437,8 +439,6 @@ intros; do 2 rewrite mem_find_b; rewrite remove_o; unfold eqb. destruct (eq_dec x y); auto. Qed. -Notation option_map := option_map (compat "8.4"). - Lemma map_o : forall m x (f:elt->elt'), find x (map f m) = option_map f (find x m). Proof. -- cgit v1.2.3 From 32ed349b992710da136a443c8e0778a6346aa9a7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 18 Jun 2016 17:47:52 -0400 Subject: Fix indentation of configure printout --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index aa26075b7..eb58e67d0 100644 --- a/configure.ml +++ b/configure.ml @@ -952,7 +952,7 @@ let print_summary () = pr "\n"; pr " Architecture : %s\n" arch; if operating_system <> "" then - pr " Operating system : %s\n" operating_system; + pr " Operating system : %s\n" operating_system; pr " Coq VM bytecode link flags : %s\n" (String.concat " " vmbyteflags); pr " Other bytecode link flags : %s\n" custom_flag; pr " OS dependent libraries : %s\n" osdeplibs; -- cgit v1.2.3 From f106e198e6adc20bc5eebbd69bb2bc2a171b82c7 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 18 Jun 2016 16:38:41 -0400 Subject: Deduplicate some names in .mailmap --- .mailmap | 3 +++ 1 file changed, 3 insertions(+) diff --git a/.mailmap b/.mailmap index c9ca597c7..51c8778f8 100644 --- a/.mailmap +++ b/.mailmap @@ -52,6 +52,7 @@ Pierre Letouzey letouzey amahboub Evgeny Makarov emakarov Gregory Malecha Gregory Malecha +Gregory Malecha Gregory Malecha Lionel Elie Mamane lmamane Claude Marché marche Micaela Mayero mayero @@ -69,6 +70,8 @@ Pierre-Marie Pédrot ppedrot pottier Matthias Puech puech Yann Régis-Gianas regisgia +Daniel de Rauglaudre Daniel de Rauglaudre +Daniel de Rauglaudre Daniel De Rauglaudre Clément Renard clrenard Claudio Sacerdoti Coen sacerdot Vincent Siles vsiles -- cgit v1.2.3 From 0a86788a929292826bc0c7e71c57ee7c5c46f335 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jul 2016 11:23:15 +0200 Subject: Bump version number in preparation for 8.5pl2 release. --- configure.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/configure.ml b/configure.ml index eb58e67d0..aee386b49 100644 --- a/configure.ml +++ b/configure.ml @@ -11,8 +11,8 @@ #load "str.cma" open Printf -let coq_version = "8.5pl1" -let coq_macos_version = "8.5.1" (** "[...] should be a string comprised of +let coq_version = "8.5pl2" +let coq_macos_version = "8.5.2" (** "[...] should be a string comprised of three non-negative, period-separed integers [...]" *) let vo_magic = 8500 let state_magic = 58500 -- cgit v1.2.3 From 870d1e06bc27ae7b108570eeaf9707041e9ff191 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jul 2016 17:37:05 +0200 Subject: Fix typo in configure (noticed by Jason). --- configure.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/configure.ml b/configure.ml index aee386b49..6748da1d8 100644 --- a/configure.ml +++ b/configure.ml @@ -13,7 +13,7 @@ open Printf let coq_version = "8.5pl2" let coq_macos_version = "8.5.2" (** "[...] should be a string comprised of -three non-negative, period-separed integers [...]" *) +three non-negative, period-separated integers [...]" *) let vo_magic = 8500 let state_magic = 58500 let distributed_exec = ["coqtop";"coqc";"coqchk";"coqdoc";"coqmktop";"coqworkmgr"; -- cgit v1.2.3 From 0bbc652fc15e1c27b20d3288205079ff295e21da Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jul 2016 17:37:46 +0200 Subject: Update csdp.cache. --- test-suite/csdp.cache | Bin 76555 -> 79491 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache index 297ac255d..75dd38fde 100644 Binary files a/test-suite/csdp.cache and b/test-suite/csdp.cache differ -- cgit v1.2.3 From 3f64bf1be849d1c4040b4d06a3417abd1a57f7d2 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 7 Jul 2016 17:54:03 +0200 Subject: Do not display goals in -compile-verbose mode (bug #4841). The -verbose family of options is only meant to echo sentences as they are processed. The patch below broke this, while fixing another issue. That other issue will be fixed in the next commit. Revert "Fixing "Load" without "Verbose" in coqtop, after vernac_com lost its" This reverts commit 2a28c677c3c205ff453b7b5903e4c22f4de2649b. --- toplevel/vernac.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index 7c4920dfb..f80aedbf3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -199,7 +199,7 @@ let display_cmd_header loc com = str " [" ++ str cmd ++ str "] "); Pp.flush_all () -let rec vernac_com verbose checknav (loc,com) = +let rec vernac_com checknav (loc,com) = let interp = function | VernacLoad (verbosely, fname) -> let fname = Envars.expand_path_macros ~warn:(fun x -> msg_warning (str x)) fname in @@ -223,7 +223,7 @@ let rec vernac_com verbose checknav (loc,com) = | v when !just_parsing -> () - | v -> Stm.interp verbose (loc,v) + | v -> Stm.interp (Flags.is_verbose()) (loc,v) in try checknav loc com; @@ -250,7 +250,7 @@ and read_vernac_file verbosely s = * raised, which means that we raised the end of the file being loaded *) while true do let loc_ast = parse_sentence input in - vernac_com verbosely checknav loc_ast; + vernac_com checknav loc_ast; pp_flush () done with any -> (* whatever the exception *) @@ -275,7 +275,7 @@ let checknav loc ast = if is_deep_navigation_vernac ast then user_error loc "Navigation commands forbidden in nested commands" -let eval_expr loc_ast = vernac_com (Flags.is_verbose()) checknav loc_ast +let eval_expr loc_ast = vernac_com checknav loc_ast (* XML output hooks *) let (f_xml_start_library, xml_start_library) = Hook.make ~default:ignore () -- cgit v1.2.3 From 947b30150602ba951efa4717d30d4a380482a963 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 7 Jul 2016 17:55:00 +0200 Subject: Prevent "Load" from displaying all the intermediate subgoals. Note that even "Load Verbose" is not supposed to display them. --- toplevel/vernac.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f80aedbf3..1f7b947e9 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -213,7 +213,7 @@ let rec vernac_com checknav (loc,com) = end; begin try - read_vernac_file verbosely f; + Flags.silently (read_vernac_file verbosely) f; restore_translator_coqdoc st; with reraise -> let reraise = Errors.push reraise in -- cgit v1.2.3