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 abe34e282ee0a5f9cca3ea9f527b254388de2cf9 Mon Sep 17 00:00:00 2001 From: thery Date: Wed, 6 Jul 2016 10:01:49 +0200 Subject: Bug Fixes : 4851 4858 4880 for nsatz the function in_ideal of ideal.ml supposes the list of polynomials does not contain zero and is duplicate free. I force this invariant in the call of in_ideal in nsatz.ml4 the function clean_pol returns the reduced list plus a list of booleans that indicates which polynomials have been deleted the function expand_pol translates back the certificate of the reduced to list to the complete list thanks to the list of booleans. The fix is quadratic with respect to the input list which should be ok for reasonable usage of nsatz. If there is some performance issue we could improve the in_pol function. --- plugins/nsatz/nsatz.ml4 | 50 +++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 48 insertions(+), 2 deletions(-) diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index ced53d82f..1230e64b9 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -472,6 +472,43 @@ let theoremedeszeros lpol p = open Ideal +(* Check if the polynomial p is in the list lp *) +let rec in_pol p lp = + match lp with + | [] -> false + | p1 :: lp1 -> if equal p p1 then true else in_pol p lp1 + +(* Remove zero polynomials and duplicates from the list of polynomials lp + Return (clp, lb) + where clp is the reduced list and lb is a list of booleans + that has the same size than lp and where true indicates an + element that has been removed + *) +let rec clean_pol lp = + match lp with + | [] -> [], [] + | p :: lp1 -> + let clp, lb = clean_pol lp1 in + if equal p zeroP || in_pol p clp then clp, true::lb + else p :: clp, false::lb + +(* Expand the list of polynomials lp putting zeros where the list of + booleans lb indicates there is a missing element + Warning: + the expansion is relative to the end of the list in reversed order + lp cannot have less elements than lb +*) +let expand_pol lb lp = + let rec aux lb lp = + match lb with + | [] -> lp + | true :: lb1 -> zeroP :: aux lb1 lp + | false :: lb1 -> + match lp with + [] -> assert false + | p :: lp1 -> p :: aux lb1 lp1 + in List.rev (aux lb (List.rev lp)) + let theoremedeszeros_termes lp = nvars:=0;(* mise a jour par term_pol_sparse *) List.iter set_nvars_term lp; @@ -522,20 +559,29 @@ let theoremedeszeros_termes lp = | [] -> assert false | p::lp1 -> let lpol = List.rev lp1 in + (* preprocessing : + we remove zero polynomials and duplicate that are not handled by in_ideal + lb is kept in order to fix the certificate in the post-processing + *) + let lpol, lb = clean_pol lpol in let (cert,lp0,p,_lct) = theoremedeszeros lpol p in info "cert ok\n"; let lc = cert.last_comb::List.rev cert.gb_comb in match remove_zeros (fun x -> equal x zeroP) lc with | [] -> assert false | (lq::lci) -> + (* post-processing : we apply the correction for the last line *) + let lq = expand_pol lb lq in (* lci commence par les nouveaux polynomes *) - let m= !nvars in + let m = !nvars in let c = pol_sparse_to_term m (polconst m cert.coef) in let r = Pow(Zero,cert.power) in let lci = List.rev lci in + (* post-processing we apply the correction for the other lines *) + let lci = List.map (expand_pol lb) lci in let lci = List.map (List.map (pol_sparse_to_term m)) lci in let lq = List.map (pol_sparse_to_term m) lq in - info ("number of parametres: "^string_of_int nparam^"\n"); + info ("number of parameters: "^string_of_int nparam^"\n"); info "term computed\n"; (c,r,lci,lq) ) -- 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 4a8c1e387bb0b971e651458319e77603d87b2d08 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 6 Jul 2016 10:46:29 +0200 Subject: Univs: fix internalization of (x := T) and casts They were allowing algebraic universes to slip in terms. --- interp/constrintern.ml | 19 ++++++++++++------- pretyping/pretyping.ml | 17 ++++++++++------- 2 files changed, 22 insertions(+), 14 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1c50253d9..28c715209 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -481,9 +481,14 @@ let intern_local_binder_aux ?(global_level=false) intern lvar (env,bl) = functio let bl' = List.map (fun a -> BDRawDef a) bl' in env, bl' @ bl | LocalRawDef((loc,na as locna),def) -> - let indef = intern env def in + let indef = intern env def in + let term, ty = + match indef with + | GCast (loc, b, Misctypes.CastConv t) -> b, t + | _ -> indef, GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None) + in (push_name_env lvar (impls_term_list indef) env locna, - (BDRawDef ((loc,(na,Explicit,Some(indef),GHole(loc,Evar_kinds.BinderType na,Misctypes.IntroAnonymous,None)))))::bl) + (BDRawDef ((loc,(na,Explicit,Some(term),ty))))::bl) | LocalPattern (loc,p,ty) -> let tyc = match ty with @@ -2030,11 +2035,11 @@ let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> + let t' = locate_if_hole (loc_of_glob_constr t) na t in + let t = + understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> - let t' = locate_if_hole (loc_of_glob_constr t) na t in - let t = - understand_tcc_evars env evdref ~expected_type:IsType t' in let d = LocalAssum (na,t) in let impls = if k == Implicit then @@ -2044,8 +2049,8 @@ let interp_rawcontext_evars env evdref k bl = in (push_rel d env, d::params, succ n, impls) | Some b -> - let c = understand_judgment_tcc env evdref b in - let d = LocalDef (na, c.uj_val, c.uj_type) in + let c = understand_tcc_evars env evdref ~expected_type:(OfType t) b in + let d = LocalDef (na, c, t) in (push_rel d env, d::params, n, impls)) (env,[],k+1,[]) (List.rev bl) in (env, par), impls diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index c8f61c66b..187eba16b 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -953,14 +953,17 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ | CastConv t | CastVM t | CastNative t -> let k = (match k with CastVM _ -> VMcast | CastNative _ -> NATIVEcast | _ -> DEFAULTcast) in let tj = pretype_type empty_valcon env evdref lvar t in - let tval = nf_evar !evdref tj.utj_val in - let cj = match k with + let tval = evd_comb1 (Evarsolve.refresh_universes + ~onlyalg:true ~status:Evd.univ_flexible (Some false) env) + evdref tj.utj_val in + let tval = nf_evar !evdref tval in + let cj, tval = match k with | VMcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in if not (occur_existential cty || occur_existential tval) then let (evd,b) = Reductionops.vm_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + if b then (evdref := evd; cj, tval) else error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) @@ -968,16 +971,16 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) env evdref (lvar : ltac_ str "unresolved arguments remain.") | NATIVEcast -> let cj = pretype empty_tycon env evdref lvar c in - let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tj.utj_val in + let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in begin let (evd,b) = Nativenorm.native_infer_conv env !evdref cty tval in - if b then (evdref := evd; cj) + if b then (evdref := evd; cj, tval) else error_actual_type_loc loc env !evdref cj tval (ConversionFailed (env,cty,tval)) end | _ -> - pretype (mk_tycon tval) env evdref lvar c + pretype (mk_tycon tval) env evdref lvar c, tval in let v = mkCast (cj.uj_val, k, tval) in { uj_val = v; uj_type = tval } -- 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 294f9928e16fd541564dbe7f36b92e0fcf2c9eff Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 6 Jul 2016 11:21:58 +0200 Subject: Fix test-suite file 3690 --- test-suite/bugs/closed/3690.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/test-suite/bugs/closed/3690.v b/test-suite/bugs/closed/3690.v index c24173abf..fd9640b89 100644 --- a/test-suite/bugs/closed/3690.v +++ b/test-suite/bugs/closed/3690.v @@ -47,7 +47,7 @@ Type@{Top.21} -> Type@{Top.23} Top.23 < Top.22 *) *) Fail Check @qux@{Set Set}. -Fail Check @qux@{Set Set Set}. +Check @qux@{Type Type Type Type}. (* [qux] should only need two universes *) -Check @qux@{i j k}. (* Error: The command has not failed!, but I think this is suboptimal *) +Check @qux@{i j k l}. (* Error: The command has not failed!, but I think this is suboptimal *) Fail Check @qux@{i j}. -- 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 9a1eb2f4fefcc52f56785f20831e854bb626ae95 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 6 Jul 2016 11:42:35 +0200 Subject: Fix #4793: Coq 8.6 should accept -compat 8.6 We also add a Coq86.v compat file. --- doc/stdlib/index-list.html.template | 1 + theories/Compat/Coq85.v | 4 ++++ theories/Compat/Coq86.v | 9 +++++++++ theories/Compat/vo.itarget | 1 + toplevel/coqinit.ml | 3 ++- toplevel/coqtop.ml | 1 + 6 files changed, 18 insertions(+), 1 deletion(-) create mode 100644 theories/Compat/Coq86.v diff --git a/doc/stdlib/index-list.html.template b/doc/stdlib/index-list.html.template index fb45777e7..9216c81fc 100644 --- a/doc/stdlib/index-list.html.template +++ b/doc/stdlib/index-list.html.template @@ -616,5 +616,6 @@ through the Require Import command.

theories/Compat/AdmitAxiom.v theories/Compat/Coq84.v theories/Compat/Coq85.v + theories/Compat/Coq86.v diff --git a/theories/Compat/Coq85.v b/theories/Compat/Coq85.v index 1e30ab919..54621cc1c 100644 --- a/theories/Compat/Coq85.v +++ b/theories/Compat/Coq85.v @@ -8,6 +8,10 @@ (** Compatibility file for making Coq act similar to Coq v8.5 *) +(** Any compatibility changes to make future versions of Coq behave like Coq 8.6 + are likely needed to make them behave like Coq 8.5. *) +Require Export Coq.Compat.Coq86. + (* In 8.5, "intros [|]", taken e.g. on a goal "A\/B->C", does not behave as "intros [H|H]" but leave instead hypotheses quantified in the goal, here producing subgoals A->C and B->C. *) diff --git a/theories/Compat/Coq86.v b/theories/Compat/Coq86.v new file mode 100644 index 000000000..6952fdf19 --- /dev/null +++ b/theories/Compat/Coq86.v @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* Flags.Current + | "8.6" -> Flags.Current + | "8.5" -> Flags.V8_5 | "8.4" -> Flags.V8_4 | "8.3" -> Flags.V8_3 | "8.2" -> Flags.V8_2 diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 7c0b9bec2..d141cd8ec 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -200,6 +200,7 @@ let require () = let add_compat_require v = match v with | Flags.V8_4 -> add_require "Coq.Compat.Coq84" + | Flags.V8_5 -> add_require "Coq.Compat.Coq85" | _ -> () let compile_list = ref ([] : (bool * string) list) -- cgit v1.2.3 From 8438b97aa5c8d8464ec7389f7992520e2c176ae6 Mon Sep 17 00:00:00 2001 From: thery Date: Wed, 6 Jul 2016 13:37:34 +0200 Subject: improved complexity in nsatz we use a hashtable to reduce the complexity of creating a duplicate-free list. --- plugins/nsatz/nsatz.ml4 | 25 +++++++++++++------------ 1 file changed, 13 insertions(+), 12 deletions(-) diff --git a/plugins/nsatz/nsatz.ml4 b/plugins/nsatz/nsatz.ml4 index 1230e64b9..592fbce67 100644 --- a/plugins/nsatz/nsatz.ml4 +++ b/plugins/nsatz/nsatz.ml4 @@ -472,12 +472,6 @@ let theoremedeszeros lpol p = open Ideal -(* Check if the polynomial p is in the list lp *) -let rec in_pol p lp = - match lp with - | [] -> false - | p1 :: lp1 -> if equal p p1 then true else in_pol p lp1 - (* Remove zero polynomials and duplicates from the list of polynomials lp Return (clp, lb) where clp is the reduced list and lb is a list of booleans @@ -485,12 +479,19 @@ let rec in_pol p lp = element that has been removed *) let rec clean_pol lp = - match lp with - | [] -> [], [] - | p :: lp1 -> - let clp, lb = clean_pol lp1 in - if equal p zeroP || in_pol p clp then clp, true::lb - else p :: clp, false::lb + let t = Hashpol.create 12 in + let find p = try Hashpol.find t p + with + Not_found -> Hashpol.add t p true; false in + let rec aux lp = + match lp with + | [] -> [], [] + | p :: lp1 -> + let clp, lb = aux lp1 in + if equal p zeroP || find p then clp, true::lb + else + (p :: clp, false::lb) in + aux lp (* Expand the list of polynomials lp putting zeros where the list of booleans lb indicates there is a missing element -- cgit v1.2.3 From a9010048c40c85b0f5e9c5fedaf2609121e71b89 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 24 May 2016 20:32:35 +0200 Subject: primproj: warning and avoid error. When defining a (co)recursive inductive with primitive projections on, which lacks eta-conversion and hence dependent elimination, build only the associated non-dependent elimination principles, and warn about this. Also make the printing of the status of an inductive w.r.t. projections and eta conversion explicit in Print and About. --- printing/prettyp.ml | 8 ++++---- tactics/elimschemes.ml | 4 ++++ tactics/elimschemes.mli | 2 ++ toplevel/indschemes.ml | 24 +++++++++++++++++++++--- 4 files changed, 31 insertions(+), 7 deletions(-) diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 1f6e99c7e..f71719cb9 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -224,12 +224,12 @@ let print_type_in_type ref = let print_primitive_record recflag mipv = function | Some (Some (_, ps,_)) -> let eta = match recflag with - | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt () - | Decl_kinds.BiFinite -> str " and has eta conversion" + | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion" + | Decl_kinds.BiFinite -> str " with eta conversion" in - [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."] + [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."] | _ -> [] - + let print_primitive ref = match ref with | IndRef ind -> diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index de2818902..99c2d8210 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -95,6 +95,10 @@ let rec_scheme_kind_from_prop = declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) + let rec_dep_scheme_kind_from_type = declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index c36797059..77f927f2d 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -13,9 +13,11 @@ open Ind_tables val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind val rec_scheme_kind_from_prop : individual scheme_kind +val rect_scheme_kind_from_type : individual scheme_kind val rect_dep_scheme_kind_from_type : individual scheme_kind val ind_scheme_kind_from_type : individual scheme_kind val ind_dep_scheme_kind_from_type : individual scheme_kind +val rec_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 32e0eb53b..8ae2140a6 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -213,11 +213,20 @@ let try_declare_beq_scheme kn = let declare_beq_scheme = declare_beq_scheme_with [] +let is_primitive_record_without_eta mib = + match mib.mind_record with + | Some (Some _) -> mib.mind_finite <> BiFinite + | _ -> false + (* Case analysis schemes *) let declare_one_case_analysis_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in - let dep = if kind == InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in + let dep = + if kind == InProp then case_scheme_kind_from_prop + else if is_primitive_record_without_eta mib then + case_scheme_kind_from_type + else case_dep_scheme_kind_from_type in let kelim = elim_sorts (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the @@ -237,15 +246,23 @@ let kinds_from_type = InProp,ind_dep_scheme_kind_from_type; InSet,rec_dep_scheme_kind_from_type] +let nondep_kinds_from_type = + [InType,rect_scheme_kind_from_type; + InProp,ind_scheme_kind_from_type; + InSet,rec_scheme_kind_from_type] + let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in let from_prop = kind == InProp in + let primwithouteta = is_primitive_record_without_eta mib in let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> if Sorts.List.mem sort kelim then Some kind else None) - (if from_prop then kinds_from_prop else kinds_from_type) in + (if from_prop then kinds_from_prop + else if primwithouteta then nondep_kinds_from_type + else kinds_from_type) in List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims @@ -502,7 +519,8 @@ let map_inductive_block f kn n = for i=0 to n-1 do f (kn,i) done let declare_default_schemes kn = let mib = Global.lookup_mind kn in let n = Array.length mib.mind_packets in - if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) && mib.mind_typing_flags.check_guarded then + if !elim_flag && (mib.mind_finite <> BiFinite || !bifinite_elim_flag) + && mib.mind_typing_flags.check_guarded then declare_induction_schemes kn; if !case_flag then map_inductive_block declare_one_case_analysis_scheme kn n; if is_eq_flag() then try_declare_beq_scheme kn; -- cgit v1.2.3 From a7ed091b6842cc78f0480504e84c3cfa261860bd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 25 May 2016 13:38:51 +0200 Subject: Move is_prim... to Inductiveops and correct Scheme Now scheme will not try to build ill-typed dependent analyses on recursive records with primitive projections but report a proper error. Minor change of the API (adding one error case to recursion_scheme_error). --- pretyping/indrec.ml | 9 ++++++++- pretyping/indrec.mli | 7 +++++-- pretyping/inductiveops.ml | 5 +++++ pretyping/inductiveops.mli | 5 ++++- toplevel/himsg.ml | 7 +++++++ toplevel/indschemes.ml | 10 ++-------- 6 files changed, 31 insertions(+), 12 deletions(-) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 0c80bd019..012c97549 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -36,6 +36,7 @@ type dep_flag = bool type recursion_scheme_error = | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive | NotMutualInScheme of inductive * inductive + | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive exception RecursionSchemeError of recursion_scheme_error @@ -483,6 +484,8 @@ let mis_make_indrec env sigma listdepkind mib u = let build_case_analysis_scheme env sigma pity dep kind = let (mib,mip) = lookup_mind_specif env (fst pity) in + if dep && Inductiveops.is_primitive_record_without_eta mib then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity))); mis_make_case_com dep env sigma pity (mib,mip) kind let is_in_prop mip = @@ -492,7 +495,7 @@ let is_in_prop mip = let build_case_analysis_scheme_default env sigma pity kind = let (mib,mip) = lookup_mind_specif env (fst pity) in - let dep = not (is_in_prop mip) in + let dep = not (is_in_prop mip || Inductiveops.is_primitive_record_without_eta mib) in mis_make_case_com dep env sigma pity (mib,mip) kind (**********************************************************************) @@ -553,6 +556,8 @@ let check_arities env listdepkind = let build_mutual_induction_scheme env sigma = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in + if dep && Inductiveops.is_primitive_record_without_eta mib then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind))); let (sp,tyi) = mind in let listdepkind = ((mind,u),mib,mip,dep,s):: @@ -572,6 +577,8 @@ let build_mutual_induction_scheme env sigma = function let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in + if dep && Inductiveops.is_primitive_record_without_eta mib then + raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind))); let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in sigma, List.hd l diff --git a/pretyping/indrec.mli b/pretyping/indrec.mli index f0736d2dd..192b64a5e 100644 --- a/pretyping/indrec.mli +++ b/pretyping/indrec.mli @@ -16,6 +16,7 @@ open Evd type recursion_scheme_error = | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * pinductive | NotMutualInScheme of inductive * inductive + | NotAllowedDependentAnalysis of (*isrec:*) bool * inductive exception RecursionSchemeError of recursion_scheme_error @@ -28,13 +29,15 @@ type dep_flag = bool val build_case_analysis_scheme : env -> 'r Sigma.t -> pinductive -> dep_flag -> sorts_family -> (constr, 'r) Sigma.sigma -(** Build a dependent case elimination predicate unless type is in Prop *) +(** Build a dependent case elimination predicate unless type is in Prop + or is a recursive record with primitive projections. *) val build_case_analysis_scheme_default : env -> 'r Sigma.t -> pinductive -> sorts_family -> (constr, 'r) Sigma.sigma (** Builds a recursive induction scheme (Peano-induction style) in the same - sort family as the inductive family; it is dependent if not in Prop *) + sort family as the inductive family; it is dependent if not in Prop + or a recursive record with primitive projections. *) val build_induction_scheme : env -> evar_map -> pinductive -> dep_flag -> sorts_family -> evar_map * constr diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index fbad0d949..64932145e 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -269,6 +269,11 @@ let projection_nparams_env env p = let projection_nparams p = projection_nparams_env (Global.env ()) p +let is_primitive_record_without_eta mib = + match mib.mind_record with + | Some (Some _) -> mib.mind_finite <> Decl_kinds.BiFinite + | _ -> false + (* Annotation for cases *) let make_case_info env ind style = let (mib,mip) = Inductive.lookup_mind_specif env ind in diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index d25f8a837..6c49099a8 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -126,7 +126,10 @@ val allowed_sorts : env -> inductive -> sorts_family list val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> - constr -> types -> types + constr -> types -> types + +(** Recursive records with primitive projections do not have eta-conversion *) +val is_primitive_record_without_eta : mutual_inductive_body -> bool (** Extract information from an inductive family *) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 1e4c3c8f1..b3eae3765 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -1147,6 +1147,11 @@ let error_not_allowed_case_analysis isrec kind i = strbrk " is not allowed for inductive definition " ++ pr_inductive (Global.env()) (fst i) ++ str "." +let error_not_allowed_dependent_analysis isrec i = + str "Dependent " ++ str (if isrec then "Induction" else "Case analysis") ++ + strbrk " is not allowed for inductive definition " ++ + pr_inductive (Global.env()) i ++ str "." + let error_not_mutual_in_scheme ind ind' = if eq_ind ind ind' then str "The inductive type " ++ pr_inductive (Global.env()) ind ++ @@ -1178,6 +1183,8 @@ let explain_recursion_scheme_error = function | NotAllowedCaseAnalysis (isrec,k,i) -> error_not_allowed_case_analysis isrec k i | NotMutualInScheme (ind,ind')-> error_not_mutual_in_scheme ind ind' + | NotAllowedDependentAnalysis (isrec, i) -> + error_not_allowed_dependent_analysis isrec i (* Pattern-matching errors *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index 8ae2140a6..ecee2e540 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -213,18 +213,13 @@ let try_declare_beq_scheme kn = let declare_beq_scheme = declare_beq_scheme_with [] -let is_primitive_record_without_eta mib = - match mib.mind_record with - | Some (Some _) -> mib.mind_finite <> BiFinite - | _ -> false - (* Case analysis schemes *) let declare_one_case_analysis_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in let dep = if kind == InProp then case_scheme_kind_from_prop - else if is_primitive_record_without_eta mib then + else if Inductiveops.is_primitive_record_without_eta mib then case_scheme_kind_from_type else case_dep_scheme_kind_from_type in let kelim = elim_sorts (mib,mip) in @@ -255,7 +250,7 @@ let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in let from_prop = kind == InProp in - let primwithouteta = is_primitive_record_without_eta mib in + let primwithouteta = Inductiveops.is_primitive_record_without_eta mib in let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> @@ -409,7 +404,6 @@ let do_mutual_induction_scheme lnamedepindsort = let sigma, listdecl = Indrec.build_mutual_induction_scheme env0 sigma lrecspec in let declare decl fi lrecref = let decltype = Retyping.get_type_of env0 sigma decl in - (* let decltype = refresh_universes decltype in *) let proof_output = Future.from_val ((decl,Univ.ContextSet.empty),Safe_typing.empty_private_constants) in let cst = define fi UserIndividualRequest sigma proof_output (Some decltype) in ConstRef cst :: lrecref -- cgit v1.2.3 From f77c2b488ca552b2316d4ebab1c051cb5a1347ab Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 25 May 2016 13:49:50 +0200 Subject: Renaming to more generic has_dependent_elim test --- pretyping/indrec.ml | 8 ++++---- pretyping/inductiveops.ml | 6 +++--- pretyping/inductiveops.mli | 6 ++++-- toplevel/indschemes.ml | 8 ++++---- 4 files changed, 15 insertions(+), 13 deletions(-) diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 012c97549..45eaae124 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -484,7 +484,7 @@ let mis_make_indrec env sigma listdepkind mib u = let build_case_analysis_scheme env sigma pity dep kind = let (mib,mip) = lookup_mind_specif env (fst pity) in - if dep && Inductiveops.is_primitive_record_without_eta mib then + if dep && not (Inductiveops.has_dependent_elim mib) then raise (RecursionSchemeError (NotAllowedDependentAnalysis (false, fst pity))); mis_make_case_com dep env sigma pity (mib,mip) kind @@ -495,7 +495,7 @@ let is_in_prop mip = let build_case_analysis_scheme_default env sigma pity kind = let (mib,mip) = lookup_mind_specif env (fst pity) in - let dep = not (is_in_prop mip || Inductiveops.is_primitive_record_without_eta mib) in + let dep = not (is_in_prop mip || not (Inductiveops.has_dependent_elim mib)) in mis_make_case_com dep env sigma pity (mib,mip) kind (**********************************************************************) @@ -556,7 +556,7 @@ let check_arities env listdepkind = let build_mutual_induction_scheme env sigma = function | ((mind,u),dep,s)::lrecspec -> let (mib,mip) = lookup_mind_specif env mind in - if dep && Inductiveops.is_primitive_record_without_eta mib then + if dep && not (Inductiveops.has_dependent_elim mib) then raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, mind))); let (sp,tyi) = mind in let listdepkind = @@ -577,7 +577,7 @@ let build_mutual_induction_scheme env sigma = function let build_induction_scheme env sigma pind dep kind = let (mib,mip) = lookup_mind_specif env (fst pind) in - if dep && Inductiveops.is_primitive_record_without_eta mib then + if dep && not (Inductiveops.has_dependent_elim mib) then raise (RecursionSchemeError (NotAllowedDependentAnalysis (true, fst pind))); let sigma, l = mis_make_indrec env sigma [(pind,mib,mip,dep,kind)] mib (snd pind) in sigma, List.hd l diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 64932145e..e4f98e730 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -269,10 +269,10 @@ let projection_nparams_env env p = let projection_nparams p = projection_nparams_env (Global.env ()) p -let is_primitive_record_without_eta mib = +let has_dependent_elim mib = match mib.mind_record with - | Some (Some _) -> mib.mind_finite <> Decl_kinds.BiFinite - | _ -> false + | Some (Some _) -> mib.mind_finite == Decl_kinds.BiFinite + | _ -> true (* Annotation for cases *) let make_case_info env ind style = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 6c49099a8..7ef848f0d 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -122,14 +122,16 @@ val inductive_has_local_defs : inductive -> bool val allowed_sorts : env -> inductive -> sorts_family list +(** (Co)Inductive records with primitive projections do not have eta-conversion, + hence no dependent elimination. *) +val has_dependent_elim : mutual_inductive_body -> bool + (** Primitive projections *) val projection_nparams : projection -> int val projection_nparams_env : env -> projection -> int val type_of_projection_knowing_arg : env -> evar_map -> Projection.t -> constr -> types -> types -(** Recursive records with primitive projections do not have eta-conversion *) -val is_primitive_record_without_eta : mutual_inductive_body -> bool (** Extract information from an inductive family *) diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index ecee2e540..f9e6c207c 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -219,7 +219,7 @@ let declare_one_case_analysis_scheme ind = let kind = inductive_sort_family mip in let dep = if kind == InProp then case_scheme_kind_from_prop - else if Inductiveops.is_primitive_record_without_eta mib then + else if not (Inductiveops.has_dependent_elim mib) then case_scheme_kind_from_type else case_dep_scheme_kind_from_type in let kelim = elim_sorts (mib,mip) in @@ -250,14 +250,14 @@ let declare_one_induction_scheme ind = let (mib,mip) = Global.lookup_inductive ind in let kind = inductive_sort_family mip in let from_prop = kind == InProp in - let primwithouteta = Inductiveops.is_primitive_record_without_eta mib in + let depelim = Inductiveops.has_dependent_elim mib in let kelim = elim_sorts (mib,mip) in let elims = List.map_filter (fun (sort,kind) -> if Sorts.List.mem sort kelim then Some kind else None) (if from_prop then kinds_from_prop - else if primwithouteta then nondep_kinds_from_type - else kinds_from_type) in + else if depelim then kinds_from_type + else nondep_kinds_from_type) in List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims -- cgit v1.2.3 From f8a5cb590352a617de38fdd8ba5ffff7691d9841 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 25 May 2016 15:17:28 +0200 Subject: Disallow dependent case on prim records w/o eta --- pretyping/cases.ml | 12 +++--------- pretyping/indrec.ml | 25 ++++--------------------- pretyping/inductiveops.ml | 29 +++++++++++++++++++++++++++++ pretyping/inductiveops.mli | 8 ++++++++ tactics/equality.ml | 2 +- test-suite/success/primitiveproj.v | 2 ++ 6 files changed, 47 insertions(+), 31 deletions(-) diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 985ad4b0d..447a4c487 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1329,14 +1329,6 @@ let build_branch initial current realargs deps (realnames,curname) pb arsign eqn *) -let mk_case pb (ci,pred,c,brs) = - let mib = lookup_mind (fst ci.ci_ind) pb.env in - match mib.mind_record with - | Some (Some (_, cs, pbs)) -> - Reduction.beta_appvect brs.(0) - (Array.map (fun p -> mkProj (Projection.make p true, c)) cs) - | _ -> mkCase (ci,pred,c,brs) - (**********************************************************************) (* Main compiling descent *) let rec compile pb = @@ -1383,7 +1375,9 @@ and match_current pb (initial,tomatch) = pred current indt (names,dep) tomatch in let ci = make_case_info pb.env (fst mind) pb.casestyle in let pred = nf_betaiota !(pb.evdref) pred in - let case = mk_case pb (ci,pred,current,brvals) in + let case = + make_case_or_project pb.env indf ci pred current brvals + in Typing.check_allowed_sort pb.env !(pb.evdref) mind current pred; { uj_val = applist (case, inst); uj_type = prod_applist typ inst } diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 45eaae124..39aeb41f7 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -43,6 +43,7 @@ exception RecursionSchemeError of recursion_scheme_error let make_prod_dep dep env = if dep then mkProd_name env else mkProd let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) + (*******************************************) (* Building curryfied elimination *) (*******************************************) @@ -376,27 +377,9 @@ let mis_make_indrec env sigma listdepkind mib u = (Anonymous,depind',concl)) arsign' in - let obj = - let projs = get_projections env indf in - match projs with - | None -> (mkCase (ci, pred, - mkRel 1, - branches)) - | Some ps -> - let branch = branches.(0) in - let ctx, br = decompose_lam_assum branch in - let n, subst = - List.fold_right (fun decl (i, subst) -> - match decl with - | LocalAssum (na,t) -> - let t = mkProj (Projection.make ps.(i) true, mkRel 1) in - i + 1, t :: subst - | LocalDef (na,b,t) -> - i, mkRel 0 :: subst) - ctx (0, []) - in - let term = substl subst br in - term + let obj = + Inductiveops.make_case_or_project env indf ci pred + (mkRel 1) branches in it_mkLambda_or_LetIn_name env obj (Termops.lift_rel_context nrec deparsign) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index e4f98e730..3fbed4b25 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -343,6 +343,35 @@ let get_projections env (ind,params) = | Some (Some (id, projs, pbs)) -> Some projs | _ -> None +let make_case_or_project env indf ci pred c branches = + let projs = get_projections env indf in + match projs with + | None -> (mkCase (ci, pred, c, branches)) + | Some ps -> + assert(Array.length branches == 1); + let () = + let _, _, t = destLambda pred in + let (ind, _), _ = dest_ind_family indf in + let mib, _ = Inductive.lookup_mind_specif env ind in + if (* dependent *) not (noccurn 1 t) && + not (has_dependent_elim mib) then + errorlabstrm "make_case_or_project" + Pp.(str"Dependent case analysis not allowed" ++ + str" on inductive type " ++ Names.MutInd.print (fst ind)) + in + let branch = branches.(0) in + let ctx, br = decompose_lam_assum branch in + let n, subst = + List.fold_right + (fun decl (i, subst) -> + match decl with + | LocalAssum (na, t) -> + let t = mkProj (Projection.make ps.(i) true, c) in + (i + 1, t :: subst) + | LocalDef (na, b, t) -> (i, substl subst b :: subst)) + ctx (0, []) + in substl subst br + (* substitution in a signature *) let substnl_rel_context subst n sign = diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli index 7ef848f0d..7bd616591 100644 --- a/pretyping/inductiveops.mli +++ b/pretyping/inductiveops.mli @@ -180,6 +180,14 @@ val type_case_branches_with_names : (** Annotation for cases *) val make_case_info : env -> inductive -> case_style -> case_info +(** Make a case or substitute projections if the inductive type is a record + with primitive projections. + Fail with an error if the elimination is dependent while the + inductive type does not allow dependent elimination. *) +val make_case_or_project : + env -> inductive_family -> case_info -> + (* pred *) constr -> (* term *) constr -> (* branches *) constr array -> constr + (*i Compatibility val make_default_case_info : env -> case_style -> inductive -> case_info i*) diff --git a/tactics/equality.ml b/tactics/equality.ml index f18de92c0..4aa7ffa7b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -860,7 +860,7 @@ let descend_then env sigma head dirn = List.map build_branch (List.interval 1 (Array.length mip.mind_consnames)) in let ci = make_case_info env ind RegularStyle in - mkCase (ci, p, head, Array.of_list brl))) + Inductiveops.make_case_or_project env indf ci p head (Array.of_list brl))) (* Now we need to construct the discriminator, given a discriminable position. This boils down to: diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index b5e6ccd61..473d37eb3 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -47,7 +47,9 @@ Check _.(next) : option Y. Lemma eta_ind (y : Y) : y = Build_Y y.(next). Proof. Fail reflexivity. Abort. +Record Fdef := { Fa : nat ; Fb := Fa; Fc : nat }. +Scheme Fdef_rec := Induction for Fdef Sort Prop. (* Rules for parsing and printing of primitive projections and their eta expansions. -- cgit v1.2.3 From f46f4ecec94953930fca6bbbc9fdb83a7a1025fc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 25 May 2016 15:24:22 +0200 Subject: Fixed bug #4622. --- test-suite/bugs/closed/4622.v | 24 ++++++++++++++++++++++++ test-suite/success/primitiveproj.v | 4 ++-- 2 files changed, 26 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4622.v diff --git a/test-suite/bugs/closed/4622.v b/test-suite/bugs/closed/4622.v new file mode 100644 index 000000000..ffa478cb8 --- /dev/null +++ b/test-suite/bugs/closed/4622.v @@ -0,0 +1,24 @@ +Set Primitive Projections. + +Record foo : Type := bar { x : unit }. + +Goal forall t u, bar t = bar u -> t = u. +Proof. + intros. + injection H. + trivial. +Qed. +(* Was: Error: Pattern-matching expression on an object of inductive type foo has invalid information. *) + +(** Dependent pattern-matching is ok on this one as it has eta *) +Definition baz (x : foo) := + match x as x' return x' = x' with + | bar u => eq_refl + end. + +Inductive foo' : Type := bar' {x' : unit; y: foo'}. +(** Dependent pattern-matching is not ok on this one *) +Fail Definition baz' (x : foo') := + match x as x' return x' = x' with + | bar' u y => eq_refl + end. diff --git a/test-suite/success/primitiveproj.v b/test-suite/success/primitiveproj.v index 473d37eb3..2fa770494 100644 --- a/test-suite/success/primitiveproj.v +++ b/test-suite/success/primitiveproj.v @@ -47,9 +47,9 @@ Check _.(next) : option Y. Lemma eta_ind (y : Y) : y = Build_Y y.(next). Proof. Fail reflexivity. Abort. -Record Fdef := { Fa : nat ; Fb := Fa; Fc : nat }. +Inductive Fdef := { Fa : nat ; Fb := Fa; Fc : Fdef }. -Scheme Fdef_rec := Induction for Fdef Sort Prop. +Fail Scheme Fdef_rec := Induction for Fdef Sort Prop. (* Rules for parsing and printing of primitive projections and their eta expansions. -- cgit v1.2.3 From df24a81b255190493281ffdeeef36754b076e9cd Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 4 Jul 2016 14:36:31 +0200 Subject: Fix reopened bug #3317. --- pretyping/inductiveops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 3fbed4b25..214e19fec 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -360,7 +360,7 @@ let make_case_or_project env indf ci pred c branches = str" on inductive type " ++ Names.MutInd.print (fst ind)) in let branch = branches.(0) in - let ctx, br = decompose_lam_assum branch in + let ctx, br = decompose_lam_n_assum (Array.length ps) branch in let n, subst = List.fold_right (fun decl (i, subst) -> -- 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 2d06b0d8ed38a2c7bc819b418af070cfe865a1d8 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 7 Jul 2016 10:38:52 +0200 Subject: Program: fix #4873: transparency option not used --- interp/constrintern.ml | 16 ++++++---- test-suite/bugs/closed/4873.v | 72 +++++++++++++++++++++++++++++++++++++++++++ toplevel/obligations.ml | 13 ++++---- 3 files changed, 88 insertions(+), 13 deletions(-) create mode 100644 test-suite/bugs/closed/4873.v diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1c50253d9..c0c38a183 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1609,11 +1609,13 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = (merge_impargs l args) loc | CRecord (loc, fs) -> - let fields = - sort_fields ~complete:true loc fs - (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark (Evar_kinds.Define true)), Misctypes.IntroAnonymous, None)) - in - begin + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + let fields = + sort_fields ~complete:true loc fs + (fun _idx -> CHole (loc, Some (Evar_kinds.QuestionMark st), + Misctypes.IntroAnonymous, None)) + in + begin match fields with | None -> user_err_loc (loc, "intern", str"No constructor inference.") | Some (n, constrname, args) -> @@ -1683,7 +1685,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = GIf (loc, c', (na', p'), intern env b1, intern env b2) | CHole (loc, k, naming, solve) -> let k = match k with - | None -> Evar_kinds.QuestionMark (Evar_kinds.Define true) + | None -> + let st = Evar_kinds.Define (not (Program.get_proofs_transparency ())) in + Evar_kinds.QuestionMark st | Some k -> k in let solve = match solve with diff --git a/test-suite/bugs/closed/4873.v b/test-suite/bugs/closed/4873.v new file mode 100644 index 000000000..f2f917b4e --- /dev/null +++ b/test-suite/bugs/closed/4873.v @@ -0,0 +1,72 @@ +Require Import Coq.Classes.Morphisms. +Require Import Relation_Definitions. +Require Import Coq.Compat.Coq85. + +Fixpoint tuple' T n : Type := + match n with + | O => T + | S n' => (tuple' T n' * T)%type + end. + +Definition tuple T n : Type := + match n with + | O => unit + | S n' => tuple' T n' + end. + +Fixpoint to_list' {T} (n:nat) {struct n} : tuple' T n -> list T := + match n with + | 0 => fun x => (x::nil)%list + | S n' => fun xs : tuple' T (S n') => let (xs', x) := xs in (x :: to_list' n' xs')%list + end. + +Definition to_list {T} (n:nat) : tuple T n -> list T := + match n with + | 0 => fun _ => nil + | S n' => fun xs : tuple T (S n') => to_list' n' xs + end. + +Program Fixpoint from_list' {T} (y:T) (n:nat) (xs:list T) : length xs = n -> tuple' T n := + match n return _ with + | 0 => + match xs return (length xs = 0 -> tuple' T 0) with + | nil => fun _ => y + | _ => _ (* impossible *) + end + | S n' => + match xs return (length xs = S n' -> tuple' T (S n')) with + | cons x xs' => fun _ => (from_list' x n' xs' _, y) + | _ => _ (* impossible *) + end + end. +Goal True. + pose from_list'_obligation_3 as e. + repeat (let e' := fresh in + rename e into e'; + (pose (e' nat) as e || pose (e' 0) as e || pose (e' nil) as e || pose (e' eq_refl) as e); + subst e'). + progress hnf in e. + pose (eq_refl : e = eq_refl). + exact I. +Qed. + +Program Definition from_list {T} (n:nat) (xs:list T) : length xs = n -> tuple T n := +match n return _ with +| 0 => + match xs return (length xs = 0 -> tuple T 0) with + | nil => fun _ : 0 = 0 => tt + | _ => _ (* impossible *) + end +| S n' => + match xs return (length xs = S n' -> tuple T (S n')) with + | cons x xs' => fun _ => from_list' x n' xs' _ + | _ => _ (* impossible *) + end +end. + +Lemma to_list_from_list : forall {T} (n:nat) (xs:list T) pf, to_list n (from_list n xs pf) = xs. +Proof. + destruct xs; simpl; intros; subst; auto. + generalize dependent t. simpl in *. + induction xs; simpl in *; intros; congruence. +Qed. \ No newline at end of file diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml index 1f1be243e..29d745732 100644 --- a/toplevel/obligations.ml +++ b/toplevel/obligations.ml @@ -858,18 +858,17 @@ let obligation_terminator name num guard hook auto pf = in let obl = { obl with obl_status = false, status } in let uctx = Evd.evar_context_universe_context ctx in - let (def, obl) = declare_obligation prg obl body ty uctx in + let (_, obl) = declare_obligation prg obl body ty uctx in let obls = Array.copy obls in let _ = obls.(num) <- obl in try ignore (update_obls prg obls (pred rem)); - if def then - if pred rem > 0 then - begin - let deps = dependencies obls num in - if not (Int.Set.is_empty deps) then + if pred rem > 0 then + begin + let deps = dependencies obls num in + if not (Int.Set.is_empty deps) then ignore (auto (Some name) None deps) - end + end with e when CErrors.noncritical e -> let e = CErrors.push e in pperror (CErrors.iprint (ExplainErr.process_vernac_interp_error e)) -- cgit v1.2.3 From 8b890de3642bee1140b238348dd76138b3f1a3dc Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 7 Jul 2016 15:49:29 +0200 Subject: Do not use implicit type info for (x := t) bindings This maintains compatibility, it is debatable if we should use implicit type information for lets to allow for coercions to fire. (Problem found in math-comp). --- interp/constrintern.ml | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 28c715209..270109e52 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -2035,9 +2035,11 @@ let interp_rawcontext_evars env evdref k bl = let (env, par, _, impls) = List.fold_left (fun (env,params,n,impls) (na, k, b, t) -> - let t' = locate_if_hole (loc_of_glob_constr t) na t in - let t = - understand_tcc_evars env evdref ~expected_type:IsType t' in + let t' = + if Option.is_empty b then locate_if_hole (loc_of_glob_constr t) na t + else t + in + let t = understand_tcc_evars env evdref ~expected_type:IsType t' in match b with None -> let d = LocalAssum (na,t) in -- 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 From 2dc63a6f49ea30e175ead4603c93cda4b2bb889b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 7 Jul 2016 08:32:36 +0200 Subject: Update COPYRIGHT. --- COPYRIGHT | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/COPYRIGHT b/COPYRIGHT index 006ce18f1..301bc7a39 100644 --- a/COPYRIGHT +++ b/COPYRIGHT @@ -1,6 +1,6 @@ The Coq proof assistant -Copyright 1999-2015 The Coq development team, INRIA, CNRS, University +Copyright 1999-2016 The Coq development team, INRIA, CNRS, University Paris Sud, University Paris 7, Ecole Polytechnique. This product includes also software developed by -- cgit v1.2.3 From 1ef6104cf043ec839059cddfe530a81418a3d474 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 7 Jul 2016 13:45:32 +0200 Subject: Add test file for #4880. --- test-suite/bugs/closed/4880.v | 11 +++++++++++ 1 file changed, 11 insertions(+) create mode 100644 test-suite/bugs/closed/4880.v diff --git a/test-suite/bugs/closed/4880.v b/test-suite/bugs/closed/4880.v new file mode 100644 index 000000000..5569798d5 --- /dev/null +++ b/test-suite/bugs/closed/4880.v @@ -0,0 +1,11 @@ +Require Import Coq.Reals.Reals Coq.nsatz.Nsatz. +Local Open Scope R. + +Goal forall x y : R, + x*x = y * y -> + x*x = -y * -y -> + x*(x*x) = 0 -> (* The associativity does not actually matter, *) + (x*x)*x = 0. (* just otherwise [assumption] would solve the goal. *) +Proof. + nsatz. +Qed. -- cgit v1.2.3 From 88f4ca3d1798fc28f230f749665bcf48597accc3 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 7 Jul 2016 13:48:20 +0200 Subject: Test file for #4858. --- test-suite/bugs/closed/4858.v | 7 +++++++ 1 file changed, 7 insertions(+) create mode 100644 test-suite/bugs/closed/4858.v diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v new file mode 100644 index 000000000..c04895a1b --- /dev/null +++ b/test-suite/bugs/closed/4858.v @@ -0,0 +1,7 @@ +Require Import Nsatz. +Goal True. +nsatz_compute + (PEc 0%Z :: PEc (-1)%Z + :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1 + :: PEsub (PEX Z 1) (PEX Z 1) :: nil). +Abort. -- cgit v1.2.3 From b0e81d65b85c1846a961196d70cd86ede2993c5b Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 8 Jul 2016 10:40:03 +0200 Subject: Update csdp.cache. --- test-suite/csdp.cache | Bin 79491 -> 79491 bytes 1 file changed, 0 insertions(+), 0 deletions(-) diff --git a/test-suite/csdp.cache b/test-suite/csdp.cache index 75dd38fde..8e5708cf0 100644 Binary files a/test-suite/csdp.cache and b/test-suite/csdp.cache differ -- cgit v1.2.3 From 8b5cab33d9877f51a5b3e1f2428c08fd07302352 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 8 Jul 2016 12:04:56 +0200 Subject: Typo in a comment of stdlib. --- theories/Logic/EqdepFacts.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 30e26c7c6..bd59159bb 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -164,7 +164,7 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent tco a dependent pair of equalities *) +(** Dependent equality is equivalent to a dependent pair of equalities *) Set Implicit Arguments. -- cgit v1.2.3 From 1a4a6f8947afaceb1f7a7f63d31e4d9a7d585db2 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 8 Jul 2016 12:05:05 +0200 Subject: Fixing #4906 (regression in printing an error message). --- engine/proofview.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/engine/proofview.ml b/engine/proofview.ml index 905e1c079..576569cf5 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -366,8 +366,9 @@ let _ = CErrors.register_handler begin function | NoSuchGoals n -> let suffix = !nosuchgoals_hook n in CErrors.errorlabstrm "" - (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix) - | _ -> raise CErrors.Unhandled + (str "No such " ++ str (String.plural n "goal") ++ str "." ++ + pr_non_empty_arg (fun x -> x) suffix) + | _ -> raise CErrors.Unhandled end (** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where -- cgit v1.2.3 From e1661dc9a43b34526437e9bc3029e6320e09f899 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 8 Jul 2016 13:03:16 +0200 Subject: Fix test file for #4858. --- test-suite/bugs/closed/4858.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/test-suite/bugs/closed/4858.v b/test-suite/bugs/closed/4858.v index c04895a1b..a2fa93832 100644 --- a/test-suite/bugs/closed/4858.v +++ b/test-suite/bugs/closed/4858.v @@ -1,6 +1,6 @@ Require Import Nsatz. Goal True. -nsatz_compute +try nsatz_compute (PEc 0%Z :: PEc (-1)%Z :: PEpow (PEsub (PEX Z 2) (PEX Z 3)) 1 :: PEsub (PEX Z 1) (PEX Z 1) :: nil). -- cgit v1.2.3 From 78063b84f46de33de8ad58f80e45a90fa290dcd6 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Fri, 8 Jul 2016 14:50:32 +0200 Subject: Add a few fixes in CHANGES that were forgotten. We should really automate the generation of the log of fixes for CHANGES. --- CHANGES | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CHANGES b/CHANGES index 7d5691efe..e7620dd4a 100644 --- a/CHANGES +++ b/CHANGES @@ -20,6 +20,12 @@ Other bugfixes - #4818: "Admitted" fails due to undefined universe anomaly after calling "destruct" - #4823: remote counter: avoid thread race on sockets +- #4841: -verbose flag changed semantics in 8.5, is much harder to use +- #4851: [nsatz] cannot handle duplicated hypotheses +- #4858: Anomaly: Uncaught exception Failure("hd"). Please report. in variant + of nsatz +- #4880: [nsatz_compute] generates invalid certificates if given redundant + hypotheses - #4881: synchronizing "Declare Implicit Tactic" with backtrack. - #4882: anomaly with Declare Implicit Tactic on hole of type with evars - Fix use of "Declare Implicit Tactic" in refine. -- cgit v1.2.3 From cb2b5cc48d54ada8a2899d311253fcb12a81fd14 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 Jul 2016 18:06:30 +0200 Subject: Remove spurious warnings about projections when requiring modules. --- pretyping/recordops.ml | 18 ++++++++++-------- 1 file changed, 10 insertions(+), 8 deletions(-) diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml index 682a88333..284af0cb1 100644 --- a/pretyping/recordops.ml +++ b/pretyping/recordops.ml @@ -195,7 +195,7 @@ let warn_projection_no_head_constant = ++ con_pp ++ str " of " ++ proji_sp_pp ++ strbrk ", ignoring it.") (* Intended to always succeed *) -let compute_canonical_projections (con,ind) = +let compute_canonical_projections warn (con,ind) = let env = Global.env () in let ctx = Univ.instantiate_univ_context (Environ.constant_context env con) in let u = Univ.UContext.instance ctx in @@ -222,7 +222,7 @@ let compute_canonical_projections (con,ind) = with Not_found -> let con_pp = Nametab.pr_global_env Id.Set.empty (ConstRef con) and proji_sp_pp = Nametab.pr_global_env Id.Set.empty (ConstRef proji_sp) in - warn_projection_no_head_constant (t,con_pp,proji_sp_pp); + if warn then warn_projection_no_head_constant (t,con_pp,proji_sp_pp); l end | _ -> l) @@ -246,9 +246,8 @@ let warn_redundant_canonical_projection = ++ strbrk " by " ++ prj ++ strbrk " in " ++ new_can_s ++ strbrk ": redundant with " ++ old_can_s) -let open_canonical_structure i (_,o) = - if Int.equal i 1 then - let lo = compute_canonical_projections o in +let add_canonical_structure warn o = + let lo = compute_canonical_projections warn o in List.iter (fun ((proj,(cs_pat,_ as pat)),s) -> let l = try Refmap.find proj !object_table with Not_found -> [] in let ocs = try Some (assoc_pat cs_pat l) @@ -260,11 +259,14 @@ let open_canonical_structure i (_,o) = and new_can_s = (Termops.print_constr s.o_DEF) in let prj = (Nametab.pr_global_env Id.Set.empty proj) and hd_val = (pr_cs_pattern cs_pat) in - warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) + if warn then warn_redundant_canonical_projection (hd_val,prj,new_can_s,old_can_s)) lo -let cache_canonical_structure o = - open_canonical_structure 1 o +let open_canonical_structure i (_, o) = + if Int.equal i 1 then add_canonical_structure false o + +let cache_canonical_structure (_, o) = + add_canonical_structure true o let subst_canonical_structure (subst,(cst,ind as obj)) = (* invariant: cst is an evaluable reference. Thus we can take *) -- cgit v1.2.3 From 5e5293eb71610290c466e6e123476b89bd7693f3 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 Jul 2016 23:11:59 +0200 Subject: Adding a breaking space in warning names. --- lib/cWarnings.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/cWarnings.ml b/lib/cWarnings.ml index 7b8dc2b9b..78fa84f33 100644 --- a/lib/cWarnings.ml +++ b/lib/cWarnings.ml @@ -48,7 +48,7 @@ let create ~name ~category ?(default=Enabled) pp = CErrors.user_err_loc (loc,"_",pp x) | Enabled -> let msg = - pp x ++ str " [" ++ str name ++ str "," ++ + pp x ++ spc () ++ str "[" ++ str name ++ str "," ++ str category ++ str "]" in let loc = Option.default !current_loc loc in -- cgit v1.2.3 From 52fee346200228d8fa05f1708bb85233f12c7b81 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 8 Jul 2016 23:13:24 +0200 Subject: Fixing the printing of unknown locations by adding a newline. --- lib/pp.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/pp.ml b/lib/pp.ml index f1eb4c059..7f4bc149d 100644 --- a/lib/pp.ml +++ b/lib/pp.ml @@ -204,7 +204,7 @@ let pr_loc_pos loc = int (fst loc) ++ str"-" ++ int (snd loc) let pr_loc loc = - if Loc.is_ghost loc then str"" + if Loc.is_ghost loc then str"" ++ fnl () else let fname = loc.Loc.fname in if CString.equal fname "" then -- cgit v1.2.3 From 3986eabe91a1b2b9280a711d1de86f331985c158 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 11 Jul 2016 16:16:20 +0200 Subject: Removing "VERBOSE=" from "Makefile.build" --- Makefile.build | 17 ++++++++++++++--- 1 file changed, 14 insertions(+), 3 deletions(-) diff --git a/Makefile.build b/Makefile.build index ebf2996f1..719046f99 100644 --- a/Makefile.build +++ b/Makefile.build @@ -59,7 +59,13 @@ DEPENDENCIES := \ # Variables meant to be modifiable via the command-line of make -VERBOSE= +# If you do: +# +# VERBOSE=1 make +# +# then instead of shortened version of the commands run by make +# you will see the actual commands. + NO_RECOMPILE_ML4= NO_RECALC_DEPS= READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary @@ -90,8 +96,13 @@ BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile # or only abbreviated versions. # Quiet mode is ON by default except if VERBOSE=1 option is given to make -SHOW := $(if $(VERBOSE),@true "",@echo "") -HIDE := $(if $(VERBOSE),,@) +ifdef VERBOSE +SHOW := @true "" +HIDE := +else +SHOW := @echo "" +HIDE := @ +endif LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) -- cgit v1.2.3 From bd3bd1ae01bea76e0d5c4540721f7160efc3c8a8 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Tue, 12 Jul 2016 10:04:56 +0200 Subject: Removing "READABLE_ML4=" from "Makefile.build" --- Makefile.build | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/Makefile.build b/Makefile.build index 719046f99..f9f64071c 100644 --- a/Makefile.build +++ b/Makefile.build @@ -66,9 +66,15 @@ DEPENDENCIES := \ # then instead of shortened version of the commands run by make # you will see the actual commands. +# If you do: +# +# READABLE_ML4=1 make +# +# then *.ml files corresponding to *.ml4 files will be generated +# in a human-readable format rather than in the binary format. + NO_RECOMPILE_ML4= NO_RECALC_DEPS= -READABLE_ML4= # non-empty means .ml of .ml4 will be ascii instead of binary VALIDATE= COQ_XML= # is "-xml" when building XML library @@ -156,7 +162,11 @@ else CAMLP4USE=-D$(CAMLVERSION) endif -PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 +ifdef READABLE_ML4 +PR_O=pr_o.cmo +else +PR_O=pr_dump.cmo +endif SYSMOD:=str unix dynlink threads SYSCMA:=$(addsuffix .cma,$(SYSMOD)) -- cgit v1.2.3 From 8cd4ad9e333169c2a9c222cb34a2199ccba56fa4 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 11 Jul 2016 16:20:42 +0200 Subject: expanding "make help" a little bit --- Makefile | 2 ++ 1 file changed, 2 insertions(+) diff --git a/Makefile b/Makefile index 93b89a489..3b9d1e67c 100644 --- a/Makefile +++ b/Makefile @@ -117,6 +117,8 @@ help: @echo "or make archclean" @echo @echo "For make to be verbose, add VERBOSE=1" + @echo + @echo "If you want camlp{4,5} to generate human-readable files, add NO_RECOMPILE_ML4=1" UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') ifdef UNSAVED_FILES -- cgit v1.2.3 From 8eccc93ddcd94eda6b027d62d882ea256fea58ba Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 11 Jul 2016 16:41:35 +0200 Subject: removing ocamldoc-related syntax errors --- interp/notation_ops.mli | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 0f1b1a875..854e222e3 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -23,7 +23,7 @@ val subst_interpretation : val ldots_var : Id.t -(** {5 Translation back and forth between [glob_constr] and [notation_constr] *) +(** {5 Translation back and forth between [glob_constr] and [notation_constr]} *) (** Translate a [glob_constr] into a notation given the list of variables bound by the notation; also interpret recursive patterns *) @@ -40,7 +40,7 @@ val glob_constr_of_notation_constr_with_binders : Loc.t -> val glob_constr_of_notation_constr : Loc.t -> notation_constr -> glob_constr -(** {5 Matching a notation pattern against a [glob_constr] *) +(** {5 Matching a notation pattern against a [glob_constr]} *) (** [match_notation_constr] matches a [glob_constr] against a notation interpretation; raise [No_match] if the matching fails *) @@ -64,5 +64,5 @@ val match_notation_constr_ind_pattern : ((cases_pattern * subscopes) list * (cases_pattern list * subscopes) list) * (int * cases_pattern list) -(** {5 Matching a notation pattern against a [glob_constr] *) +(** {5 Matching a notation pattern against a [glob_constr]} *) -- cgit v1.2.3 From 3a3f11fe1b6c0f059cf2bd0d71aa4deb4a876b26 Mon Sep 17 00:00:00 2001 From: Matej Kosik Date: Mon, 11 Jul 2016 16:49:15 +0200 Subject: ".gitignore" update --- .gitignore | 1 + 1 file changed, 1 insertion(+) diff --git a/.gitignore b/.gitignore index 411619080..0d5eee652 100644 --- a/.gitignore +++ b/.gitignore @@ -161,3 +161,4 @@ dev/myinclude /doc/refman/Reference-Manual.optidx /doc/refman/Reference-Manual.optind user-contrib +.*.sw* -- cgit v1.2.3 From 72d9bf028d0cf40cb6c727c69bfbcc15aafc4944 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 Jul 2016 16:28:10 +0200 Subject: Makefile: no more .ml4.d hence no more rule to clean them --- Makefile | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/Makefile b/Makefile index 3b9d1e67c..34ce67b7d 100644 --- a/Makefile +++ b/Makefile @@ -159,7 +159,7 @@ Makefile $(wildcard Makefile.*) config/Makefile : ; # Cleaning ########################################################################### -.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean ml4depclean depclean cleanconfig distclean voclean devdocclean +.PHONY: clean cleankeepvo objclean cruftclean indepclean docclean archclean optclean clean-ide ml4clean depclean cleanconfig distclean voclean devdocclean clean: objclean cruftclean depclean docclean devdocclean @@ -220,9 +220,6 @@ clean-ide: ml4clean: rm -f $(GENML4FILES) -ml4depclean: - find . -name '*.ml4.d' | xargs rm -f - depclean: find . $(FIND_VCS_CLAUSE) '(' -name '*.d' ')' -print | xargs rm -f -- cgit v1.2.3 From ea25e8bcf64caac66bcbd33457ee91d56e80fea3 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 Jul 2016 16:32:12 +0200 Subject: .gitignore: no more generated grammar/*.ml files --- .gitignore | 4 ---- 1 file changed, 4 deletions(-) diff --git a/.gitignore b/.gitignore index 0d5eee652..8a0c54f8f 100644 --- a/.gitignore +++ b/.gitignore @@ -119,10 +119,6 @@ g_*.ml ide/project_file.ml parsing/compat.ml -grammar/q_util.ml -grammar/tacextend.ml -grammar/vernacextend.ml -grammar/argextend.ml parsing/cLexer.ml ltac/coretactics.ml ltac/extratactics.ml -- cgit v1.2.3 From 605048905db9107a1d4b3c35ce59f5719474f875 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Tue, 12 Jul 2016 18:17:17 +0200 Subject: Makefile.build: follow-up of commits by Matej on VERBOSE and READABLE_ML4 - With the ?= construction, we avoid warnings about undefined variables, while tolerating both 'make VERBOSE=1' and 'VERBOSE=1 make' - Some extra documentation and cleanup --- Makefile | 2 +- Makefile.build | 103 ++++++++++++++++++++++++++------------------------------- 2 files changed, 48 insertions(+), 57 deletions(-) diff --git a/Makefile b/Makefile index 34ce67b7d..6649542c8 100644 --- a/Makefile +++ b/Makefile @@ -118,7 +118,7 @@ help: @echo @echo "For make to be verbose, add VERBOSE=1" @echo - @echo "If you want camlp{4,5} to generate human-readable files, add NO_RECOMPILE_ML4=1" + @echo "If you want camlp{4,5} to generate human-readable files, add READABLE_ML4=1" UNSAVED_FILES:=$(shell find . -name '.\#*v' -o -name '.\#*.ml' -o -name '.\#*.ml?') ifdef UNSAVED_FILES diff --git a/Makefile.build b/Makefile.build index f9f64071c..95df69c2d 100644 --- a/Makefile.build +++ b/Makefile.build @@ -9,6 +9,40 @@ # This makefile is normally called by the main Makefile after setting # some variables. +########################################################################### +# User-customizable variables +########################################################################### + +# The following variables could be modified via the command-line of make, +# either with the syntax 'make XYZ=1' or 'XYZ=1 make' + +# To see the actual commands launched by make instead of shortened versions, +# set this variable to 1 (or any non-empty value): +VERBOSE ?= + +# If set to 1 (or non-empty) then *.ml files corresponding to *.ml4 files +# will be generated in a human-readable format rather than in a binary format. +READABLE_ML4 ?= + +# When non-empty, a time command is performed at each .v compilation. +# To collect compilation timings of .v and import them in a spreadsheet, +# you could hence consider: make TIMED=1 2> timings.csv +TIMED ?= + +# When $(TIMED) is set, the time command used by default is $(STDTIME) +# (see below), unless the following variable is non-empty. For instance, +# it could be set to "'/usr/bin/time -p'". +TIMECMD ?= + +# Non-empty skips the update of all dependency .d files: +NO_RECALC_DEPS ?= + +# Non-empty runs the checker on all produced .vo files: +VALIDATE ?= + +# Is "-xml" when building XML library: +COQ_XML ?= + ########################################################################### # Default starting rule ########################################################################### @@ -57,59 +91,18 @@ DEPENDENCIES := \ # Compilation options ########################################################################### -# Variables meant to be modifiable via the command-line of make - -# If you do: -# -# VERBOSE=1 make -# -# then instead of shortened version of the commands run by make -# you will see the actual commands. - -# If you do: -# -# READABLE_ML4=1 make -# -# then *.ml files corresponding to *.ml4 files will be generated -# in a human-readable format rather than in the binary format. - -NO_RECOMPILE_ML4= -NO_RECALC_DEPS= -VALIDATE= -COQ_XML= # is "-xml" when building XML library - -TIMED= # non-empty will activate a default time command - # when compiling .v (see $(STDTIME) below) - -TIMECMD= # if you prefer a specific time command instead of $(STDTIME) - # e.g. "'time -p'" +# Default timing command +STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" -# NB: if you want to collect compilation timings of .v and import them -# in a spreadsheet, I suggest something like: -# make TIMED=1 2> timings.csv +TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) # NB: do not use a variable named TIME, since this variable controls # the output format of the unix command time. For instance: # TIME="%C (%U user, %S sys, %e total, %M maxres)" -STDTIME=/usr/bin/time -f "$* (user: %U mem: %M ko)" -TIMER=$(if $(TIMED), $(STDTIME), $(TIMECMD)) - COQOPTS=$(COQ_XML) $(NATIVECOMPUTE) BOOTCOQC=$(TIMER) $(COQTOPEXE) -boot $(COQOPTS) -compile -# The SHOW and HIDE variables control whether make will echo complete commands -# or only abbreviated versions. -# Quiet mode is ON by default except if VERBOSE=1 option is given to make - -ifdef VERBOSE -SHOW := @true "" -HIDE := -else -SHOW := @echo "" -HIDE := @ -endif - LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) @@ -162,11 +155,7 @@ else CAMLP4USE=-D$(CAMLVERSION) endif -ifdef READABLE_ML4 -PR_O=pr_o.cmo -else -PR_O=pr_dump.cmo -endif +PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) SYSMOD:=str unix dynlink threads SYSCMA:=$(addsuffix .cma,$(SYSMOD)) @@ -183,6 +172,13 @@ endif # Infrastructure for the rest of the Makefile ########################################################################### +# The SHOW and HIDE variables control whether make will echo complete commands +# or only abbreviated versions. +# Quiet mode is ON by default except if VERBOSE=1 option is given to make + +SHOW := $(if $(VERBOSE),@true "",@echo "") +HIDE := $(if $(VERBOSE),,@) + define order-only-template ifeq "order-only" "$(1)" ORDER_ONLY_SEP:=| @@ -203,13 +199,8 @@ ifdef VALIDATE VO_TOOLS_DEP += $(CHICKEN) endif -ifdef NO_RECALC_DEPS - D_DEPEND_BEFORE_SRC:=| - D_DEPEND_AFTER_SRC:= -else - D_DEPEND_BEFORE_SRC:= - D_DEPEND_AFTER_SRC:=| -endif +D_DEPEND_BEFORE_SRC := $(if $(NO_RECALC_DEPS),|,) +D_DEPEND_AFTER_SRC := $(if $(NO_RECALC_DEPS),,|) ## When a rule redirects stdout of a command to the target file : cmd > $@ ## then the target file will be created even if cmd has failed. -- cgit v1.2.3 From 3f9215b2b65b902cc52fd540f57f67342401a91f Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 13 Jul 2016 09:45:41 +0200 Subject: Makefile.dev: fix a typo in the 'logic' rule --- Makefile.dev | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Makefile.dev b/Makefile.dev index 26092e8dc..501a7744a 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -134,7 +134,7 @@ ltac: ltac/ltac.cma ###################### init: $(filter theories/Init/%, $(THEORIESVO)) -logic: $(filter theories/Logic/%, %(THEORIESVO)) +logic: $(filter theories/Logic/%, $(THEORIESVO)) arith: $(filter theories/Arith/%, $(THEORIESVO)) bool: $(filter theories/Bool/%, $(THEORIESVO)) parith: $(filter theories/PArith/%, $(THEORIESVO)) -- cgit v1.2.3 From 55d32c9a017853c2411f894a3ad1a946c628ba9c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 3 Jul 2016 11:36:05 +0200 Subject: Typo. --- theories/Logic/EqdepFacts.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 30e26c7c6..bd59159bb 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -164,7 +164,7 @@ Proof. split; auto using eq_sig_eq_dep, eq_dep_eq_sig. Qed. -(** Dependent equality is equivalent tco a dependent pair of equalities *) +(** Dependent equality is equivalent to a dependent pair of equalities *) Set Implicit Arguments. -- cgit v1.2.3 From 65ba1b36df33a74998240a02fecc1fb80c3eeeee Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 13 Jul 2016 15:27:28 +0200 Subject: Fixing printing of evar name in an error message of instantiate. --- proofs/evar_refiner.ml | 2 +- test-suite/output/Errors.out | 2 ++ test-suite/output/Errors.v | 9 +++++++++ 3 files changed, 12 insertions(+), 1 deletion(-) diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml index 059ae54c9..b6f2f69d2 100644 --- a/proofs/evar_refiner.ml +++ b/proofs/evar_refiner.ml @@ -56,7 +56,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma = let loc = Glob_ops.loc_of_glob_constr rawc in user_err_loc (loc,"", str "Instance is not well-typed in the environment of " ++ - str (string_of_existential evk)) + pr_existential_key sigma evk ++ str ".") in define_and_solve_constraints evk typed_c env (evars_reset_evd sigma' sigma) diff --git a/test-suite/output/Errors.out b/test-suite/output/Errors.out index 6354ad469..8048deb0c 100644 --- a/test-suite/output/Errors.out +++ b/test-suite/output/Errors.out @@ -5,3 +5,5 @@ Unable to unify "nat" with "True". The command has indeed failed with message: In nested Ltac calls to "f" and "apply x", last call failed. Unable to unify "nat" with "True". +The command has indeed failed with message: +Error: Instance is not well-typed in the environment of ?x diff --git a/test-suite/output/Errors.v b/test-suite/output/Errors.v index 352c87385..424d24801 100644 --- a/test-suite/output/Errors.v +++ b/test-suite/output/Errors.v @@ -16,3 +16,12 @@ Goal True. Fail simpl; apply 0. Fail simpl; f 0. Abort. + +(* Test instantiate error messages *) + +Goal forall T1 (P1 : T1 -> Type), sigT P1 -> sigT P1. +intros T1 P1 H1. +eexists ?[x]. +destruct H1 as [x1 H1]. +Fail instantiate (x:=projT1 x1). +Abort. -- cgit v1.2.3