diff options
37 files changed, 219 insertions, 152 deletions
@@ -27,7 +27,10 @@ Specification language Tactics - Flag "Bracketing Last Introduction Pattern" is now on by default. -- Flag "Regular Subst Tactic" is now on by default. +- Flag "Regular Subst Tactic" is now on by default: it respects the + initial order of hypothesis, it contracts cycles, it unfolds no + local definitions (common source of incompatibilities, fixable by + "Unset Regular Subst Tactic"). - New flag "Refolding Reduction", now disabled by default, which turns on refolding of constants/fixpoints (as in cbn) during the reductions done during type inference and tactic retyping. Can be extremely diff --git a/COMPATIBILITY b/COMPATIBILITY index 892eaa599e..d423e71df3 100644 --- a/COMPATIBILITY +++ b/COMPATIBILITY @@ -11,6 +11,12 @@ Remedy: instead (compatible with 8.4). - Unset the option for the program/proof the obligation/subproof originates from. + +Symptom: In a goal, order of hypotheses, or absence of an equality of +the form "x = t" or "t = x", or no unfolding of a local definition. +Cause: This might be connected to a number of fixes in the tactic +"subst". The former behavior can be reactivated by issuing "Unset +Regular Subst Tactic". Potential sources of incompatibilities between Coq V8.4 and V8.5 ---------------------------------------------------------------- diff --git a/checker/checker.ml b/checker/checker.ml index 0c411ae44d..503697b592 100644 --- a/checker/checker.ml +++ b/checker/checker.ml @@ -209,7 +209,8 @@ let usage () = open Type_errors let anomaly_string () = str "Anomaly: " -let report () = (str "." ++ spc () ++ str "Please report.") +let report () = (str "." ++ spc () ++ str "Please report" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str ".") let guill s = str "\"" ++ str s ++ str "\"" diff --git a/config/coq_config.mli b/config/coq_config.mli index a0e1019fa8..6087c01169 100644 --- a/config/coq_config.mli +++ b/config/coq_config.mli @@ -62,6 +62,7 @@ val natdynlinkflag : string (* special cases of natdynlink (e.g. MacOS 10.5) *) val wwwcoq : string val wwwrefman : string +val wwwbugtracker : string val wwwstdlib : string val localwwwrefman : string diff --git a/configure.ml b/configure.ml index 2c1d531ead..23ec93e078 100644 --- a/configure.ml +++ b/configure.ml @@ -1043,6 +1043,7 @@ let write_configml f = pr "let with_geoproof = ref %B\n" !Prefs.geoproof; pr_s "browser" browser; pr_s "wwwcoq" !Prefs.coqwebsite; + pr_s "wwwbugtracker" (!Prefs.coqwebsite ^ "bugs/"); pr_s "wwwrefman" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/refman/"); pr_s "wwwstdlib" (!Prefs.coqwebsite ^ "distrib/" ^ coq_version ^ "/stdlib/"); pr_s "localwwwrefman" ("file:/" ^ docdir ^ "/html/refman"); diff --git a/ide/session.ml b/ide/session.ml index e998337604..fc6340d283 100644 --- a/ide/session.ml +++ b/ide/session.ml @@ -108,10 +108,10 @@ let set_buffer_handlers let id = ref 0 in fun () -> incr id; !id in let running_action = ref None in - let cancel_signal reason = + let cancel_signal ?(stop_emit=true) reason = Minilib.log ("user_action cancelled: "^reason); action_was_cancelled := true; - GtkSignal.stop_emit () in + if stop_emit then GtkSignal.stop_emit () in let del_mark () = try buffer#delete_mark (`NAME "target") with GText.No_such_mark _ -> () in @@ -124,7 +124,7 @@ let set_buffer_handlers fun () -> (* If Coq is busy due to the current action, we don't cancel *) match !running_action with | Some aid when aid = action -> () - | _ -> cancel_signal "Coq busy" in + | _ -> cancel_signal ~stop_emit:false "Coq busy" in Coq.try_grab coqtop action fallback in let get_start () = buffer#get_iter_at_mark (`NAME "start_of_input") in let get_stop () = buffer#get_iter_at_mark (`NAME "stop_of_input") in diff --git a/interp/notation.ml b/interp/notation.ml index 0798d385d4..d301ed21db 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -553,15 +553,13 @@ let ntpe_eq t1 t2 = match t1, t2 with | NtnTypeBinderList, NtnTypeBinderList -> true | (NtnTypeConstr | NtnTypeOnlyBinder | NtnTypeConstrList | NtnTypeBinderList), _ -> false - -let vars_eq (id1, (sc1, tp1)) (id2, (sc2, tp2)) = - Id.equal id1 id2 && +let var_attributes_eq (_, (sc1, tp1)) (_, (sc2, tp2)) = pair_eq (Option.equal String.equal) (List.equal String.equal) sc1 sc2 && ntpe_eq tp1 tp2 let interpretation_eq (vars1, t1) (vars2, t2) = - List.equal vars_eq vars1 vars2 && - Notation_ops.eq_notation_constr t1 t2 + List.equal var_attributes_eq vars1 vars2 && + Notation_ops.eq_notation_constr (List.map fst vars1, List.map fst vars2) t1 t2 let exists_notation_in_scope scopt ntn r = let scope = match scopt with Some s -> s | None -> default_scope in diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1f29a2948f..cc81a00919 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -47,62 +47,62 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with | GHole _ | GSort _ | GLetIn _), _ -> false -let rec eq_notation_constr t1 t2 = match t1, t2 with +let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with | NRef gr1, NRef gr2 -> eq_gr gr1 gr2 -| NVar id1, NVar id2 -> Id.equal id1 id2 +| NVar id1, NVar id2 -> Int.equal (List.index Id.equal id1 vars1) (List.index Id.equal id2 vars2) | NApp (t1, a1), NApp (t2, a2) -> - eq_notation_constr t1 t2 && List.equal eq_notation_constr a1 a2 + (eq_notation_constr vars) t1 t2 && List.equal (eq_notation_constr vars) a1 a2 | NHole (_, _, _), NHole (_, _, _) -> true (** FIXME? *) | NList (i1, j1, t1, u1, b1), NList (i2, j2, t2, u2, b2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 && b1 == b2 + Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 && b1 == b2 | NLambda (na1, t1, u1), NLambda (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NProd (na1, t1, u1), NProd (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NBinderList (i1, j1, t1, u1), NBinderList (i2, j2, t2, u2) -> - Id.equal i1 i2 && Id.equal j1 j2 && eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 + Id.equal i1 i2 && Id.equal j1 j2 && (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 | NLetIn (na1, t1, u1), NLetIn (na2, t2, u2) -> - Name.equal na1 na2 && eq_notation_constr t1 t2 && eq_notation_constr u1 u2 + Name.equal na1 na2 && (eq_notation_constr vars) t1 t2 && (eq_notation_constr vars) u1 u2 | NCases (_, o1, r1, p1), NCases (_, o2, r2, p2) -> (** FIXME? *) let eqpat (p1, t1) (p2, t2) = List.equal cases_pattern_eq p1 p2 && - eq_notation_constr t1 t2 + (eq_notation_constr vars) t1 t2 in let eqf (t1, (na1, o1)) (t2, (na2, o2)) = let eq (i1, n1) (i2, n2) = eq_ind i1 i2 && List.equal Name.equal n1 n2 in - eq_notation_constr t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 + (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && Option.equal eq o1 o2 in - Option.equal eq_notation_constr o1 o2 && + Option.equal (eq_notation_constr vars) o1 o2 && List.equal eqf r1 r2 && List.equal eqpat p1 p2 | NLetTuple (nas1, (na1, o1), t1, u1), NLetTuple (nas2, (na2, o2), t2, u2) -> List.equal Name.equal nas1 nas2 && Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 && - eq_notation_constr u1 u2 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) t1 t2 && + (eq_notation_constr vars) u1 u2 | NIf (t1, (na1, o1), u1, r1), NIf (t2, (na2, o2), u2, r2) -> - eq_notation_constr t1 t2 && + (eq_notation_constr vars) t1 t2 && Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr u1 u2 && - eq_notation_constr r1 r2 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) u1 u2 && + (eq_notation_constr vars) r1 r2 | NRec (_, ids1, ts1, us1, rs1), NRec (_, ids2, ts2, us2, rs2) -> (** FIXME? *) let eq (na1, o1, t1) (na2, o2, t2) = Name.equal na1 na2 && - Option.equal eq_notation_constr o1 o2 && - eq_notation_constr t1 t2 + Option.equal (eq_notation_constr vars) o1 o2 && + (eq_notation_constr vars) t1 t2 in Array.equal Id.equal ids1 ids2 && Array.equal (List.equal eq) ts1 ts2 && - Array.equal eq_notation_constr us1 us2 && - Array.equal eq_notation_constr rs1 rs2 + Array.equal (eq_notation_constr vars) us1 us2 && + Array.equal (eq_notation_constr vars) rs1 rs2 | NSort s1, NSort s2 -> Miscops.glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> - eq_notation_constr t1 t2 && cast_type_eq eq_notation_constr c1 c2 + (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ | NRec _ | NSort _ | NCast _), _ -> false diff --git a/interp/notation_ops.mli b/interp/notation_ops.mli index 854e222e30..4ebd3ddd80 100644 --- a/interp/notation_ops.mli +++ b/interp/notation_ops.mli @@ -12,7 +12,7 @@ open Glob_term (** {5 Utilities about [notation_constr]} *) -val eq_notation_constr : notation_constr -> notation_constr -> bool +val eq_notation_constr : Id.t list * Id.t list -> notation_constr -> notation_constr -> bool (** Substitution of kernel names in interpretation data *) diff --git a/lib/cErrors.ml b/lib/cErrors.ml index 1459141d1e..c69c7e4001 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -93,7 +93,9 @@ let print_backtrace e = match Backtrace.get_backtrace e with let print_anomaly askreport e = if askreport then - hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.") + hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ + strbrk "Please report at " ++ str Coq_config.wwwbugtracker ++ + str ".") else hov 0 (raw_anomaly e) diff --git a/lib/flags.ml b/lib/flags.ml index 13525165ab..d29064c97f 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -226,6 +226,7 @@ let print_mod_uid = ref false let tactic_context_compat = ref false let profile_ltac = ref false +let profile_ltac_cutoff = ref 0.0 let dump_bytecode = ref false let set_dump_bytecode = (:=) dump_bytecode diff --git a/lib/flags.mli b/lib/flags.mli index 8fe64d24fa..839c252cbb 100644 --- a/lib/flags.mli +++ b/lib/flags.mli @@ -149,6 +149,7 @@ val tactic_context_compat : bool ref context vs. appcontext) is set. *) val profile_ltac : bool ref +val profile_ltac_cutoff : float ref (** Dump the bytecode after compilation (for debugging purposes) *) val dump_bytecode : bool ref diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index 102918e5e5..a91ff98fb9 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -401,11 +401,11 @@ let print_results ~cutoff = print_results_filter ~cutoff ~filter:(fun _ -> true) let print_results_tactic tactic = - print_results_filter ~cutoff:0.0 ~filter:(fun s -> + print_results_filter ~cutoff:!Flags.profile_ltac_cutoff ~filter:(fun s -> String.(equal tactic (sub (s ^ ".") 0 (min (1+length s) (length tactic))))) let do_print_results_at_close () = - if get_profiling () then print_results ~cutoff:0.0 + if get_profiling () then print_results ~cutoff:!Flags.profile_ltac_cutoff let _ = Declaremods.append_end_library_hook do_print_results_at_close diff --git a/ltac/profile_ltac_tactics.ml4 b/ltac/profile_ltac_tactics.ml4 index 9083bda60a..8cb76d81c5 100644 --- a/ltac/profile_ltac_tactics.ml4 +++ b/ltac/profile_ltac_tactics.ml4 @@ -31,7 +31,7 @@ VERNAC COMMAND EXTEND ResetLtacProfiling CLASSIFIED AS SIDEFF END VERNAC COMMAND EXTEND ShowLtacProfile CLASSIFIED AS QUERY -| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:0.0 ] +| [ "Show" "Ltac" "Profile" ] -> [ print_results ~cutoff:!Flags.profile_ltac_cutoff ] | [ "Show" "Ltac" "Profile" "CutOff" int(n) ] -> [ print_results ~cutoff:(float_of_int n) ] END diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index 312c2eab3d..a980a43f53 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -371,8 +371,7 @@ and extract_really_ind env kn mib = let packets = Array.mapi (fun i mip -> - let (ind,u), ctx = - Universes.fresh_inductive_instance env (kn,i) in + let (_,u),_ = Universes.fresh_inductive_instance env (kn,i) in let ar = Inductive.type_of_inductive env ((mib,mip),u) in let info = (fst (flag_of_type env ar) = Info) in let s,v = if info then type_sign_vl env ar else [],[] in @@ -591,10 +590,10 @@ let rec extract_term env mle mlt c args = with NotDefault d -> let mle' = Mlenv.push_std_type mle (Tdummy d) in ast_pop (extract_term env' mle' mlt c2 args')) - | Const (kn,u) -> - extract_cst_app env mle mlt kn u args - | Construct (cp,u) -> - extract_cons_app env mle mlt cp u args + | Const (kn,_) -> + extract_cst_app env mle mlt kn args + | Construct (cp,_) -> + extract_cons_app env mle mlt cp args | Proj (p, c) -> let term = Retyping.expand_projection env (Evd.from_env env) p c [] in extract_term env mle mlt term args @@ -645,7 +644,7 @@ and make_mlargs env e s args typs = (*s Extraction of a constant applied to arguments. *) -and extract_cst_app env mle mlt kn u args = +and extract_cst_app env mle mlt kn args = (* First, the [ml_schema] of the constant, in expanded version. *) let nb,t = record_constant_type env kn None in let schema = nb, expand env t in @@ -718,7 +717,7 @@ and extract_cst_app env mle mlt kn u args = they are fixed, and thus are not used for the computation. \end{itemize} *) -and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) u args = +and extract_cons_app env mle mlt (((kn,i) as ip,j) as cp) args = (* First, we build the type of the constructor, stored in small pieces. *) let mi = extract_ind env kn in let params_nb = mi.ind_nparams in diff --git a/plugins/nsatz/ideal.ml b/plugins/nsatz/ideal.ml index 7c2178222f..48bdad8264 100644 --- a/plugins/nsatz/ideal.ml +++ b/plugins/nsatz/ideal.ml @@ -19,75 +19,6 @@ open Utile exception NotInIdeal -module type S = sig - -(* Monomials *) -type mon = int array - -val mult_mon : mon -> mon -> mon -val deg : mon -> int -val compare_mon : mon -> mon -> int -val div_mon : mon -> mon -> mon -val div_mon_test : mon -> mon -> bool -val ppcm_mon : mon -> mon -> mon - -(* Polynomials *) - -type deg = int -type coef -type poly -type polynom - -val repr : poly -> (coef * mon) list -val polconst : coef -> poly -val zeroP : poly -val gen : int -> poly - -val equal : poly -> poly -> bool -val name_var : string list ref -val getvar : string list -> int -> string -val lstringP : poly list -> string -val printP : poly -> unit -val lprintP : poly list -> unit - -val div_pol_coef : poly -> coef -> poly -val plusP : poly -> poly -> poly -val mult_t_pol : coef -> mon -> poly -> poly -val selectdiv : mon -> poly list -> poly -val oppP : poly -> poly -val emultP : coef -> poly -> poly -val multP : poly -> poly -> poly -val puisP : poly -> int -> poly -val contentP : poly -> coef -val contentPlist : poly list -> coef -val pgcdpos : coef -> coef -> coef -val div_pol : poly -> poly -> coef -> coef -> mon -> poly -val reduce2 : poly -> poly list -> coef * poly - -val poldepcontent : coef list ref -val coefpoldep_find : poly -> poly -> poly -val coefpoldep_set : poly -> poly -> poly -> unit -val initcoefpoldep : poly list -> unit -val reduce2_trace : poly -> poly list -> poly list -> poly list * poly -val spol : poly -> poly -> poly -val etrangers : poly -> poly -> bool -val div_ppcm : poly -> poly -> poly -> bool - -val genPcPf : poly -> poly list -> poly list -> poly list -val genOCPf : poly list -> poly list - -val is_homogeneous : poly -> bool - -type certificate = - { coef : coef; power : int; - gb_comb : poly list list; last_comb : poly list } - -val test_dans_ideal : poly -> poly list -> poly list -> - poly list * poly * certificate -val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate - -end - (*********************************************************************** Global options *) diff --git a/plugins/nsatz/ideal.mli b/plugins/nsatz/ideal.mli new file mode 100644 index 0000000000..d1a2a0a7d1 --- /dev/null +++ b/plugins/nsatz/ideal.mli @@ -0,0 +1,47 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +module Make (P : Polynom.S) : +sig +(* Polynomials *) + +type deg = int +type coef = P.t +type poly + +val repr : poly -> (coef * int array) list +val polconst : int -> coef -> poly +val zeroP : poly +val gen : int -> int -> poly + +val equal : poly -> poly -> bool +val name_var : string list ref + +val plusP : poly -> poly -> poly +val oppP : poly -> poly +val multP : poly -> poly -> poly +val puisP : poly -> int -> poly + +val poldepcontent : coef list ref + +type certificate = + { coef : coef; power : int; + gb_comb : poly list list; last_comb : poly list } + +val in_ideal : deg -> poly list -> poly -> poly list * poly * certificate + +module Hashpol : Hashtbl.S with type key = poly + +val sugar_flag : bool ref +val divide_rem_with_critical_pair : bool ref + +end + +exception NotInIdeal + +val lexico : bool ref diff --git a/plugins/nsatz/nsatz.mli b/plugins/nsatz/nsatz.mli new file mode 100644 index 0000000000..e876ccfa5d --- /dev/null +++ b/plugins/nsatz/nsatz.mli @@ -0,0 +1,9 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val nsatz_compute : Constr.t -> unit Proofview.tactic diff --git a/plugins/setoid_ring/Ncring_initial.v b/plugins/setoid_ring/Ncring_initial.v index 96885d2f7a..20022c00ec 100644 --- a/plugins/setoid_ring/Ncring_initial.v +++ b/plugins/setoid_ring/Ncring_initial.v @@ -18,7 +18,6 @@ Require Import BinInt. Require Import Setoid. Require Export Ncring. Require Export Ncring_polynom. -Import List. Set Implicit Arguments. @@ -78,7 +77,8 @@ Context {R:Type}`{Ring R}. | Z0 => 0 | Zneg p => -(gen_phiPOS p) end. - Notation "[ x ]" := (gen_phiZ x). + Local Notation "[ x ]" := (gen_phiZ x) : ZMORPHISM. + Local Open Scope ZMORPHISM. Definition get_signZ z := match z with diff --git a/plugins/setoid_ring/Ring_theory.v b/plugins/setoid_ring/Ring_theory.v index 7fcd6c08a7..f7757a18da 100644 --- a/plugins/setoid_ring/Ring_theory.v +++ b/plugins/setoid_ring/Ring_theory.v @@ -238,7 +238,6 @@ Section ALMOST_RING. Variable req : R -> R -> Prop. Notation "0" := rO. Notation "1" := rI. Infix "==" := req. Infix "+" := radd. Infix "* " := rmul. - Infix "-" := rsub. Notation "- x" := (ropp x). (** Leibniz equality leads to a setoid theory and is extensional*) Lemma Eqsth : Equivalence (@eq R). @@ -263,7 +262,7 @@ Section ALMOST_RING. -x = x and x - y = x + y *) Definition SRopp (x:R) := x. Notation "- x" := (SRopp x). - Definition SRsub x y := x + -y. Notation "x - y " := (SRsub x y). + Definition SRsub x y := x + -y. Infix "-" := SRsub. Lemma SRopp_ext : forall x y, x == y -> -x == -y. Proof. intros x y H; exact H. Qed. @@ -320,6 +319,8 @@ Section ALMOST_RING. Qed. End SEMI_RING. + Infix "-" := rsub. + Notation "- x" := (ropp x). Variable Reqe : ring_eq_ext radd rmul ropp req. Add Morphism radd : radd_ext2. exact (Radd_ext Reqe). Qed. diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 46f0219f91..48bf9149d0 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -239,10 +239,12 @@ let interp_elimination_sort = function | GSet -> InSet | GType _ -> InType +type inference_hook = env -> evar_map -> evar -> evar_map * constr + type inference_flags = { use_typeclasses : bool; use_unif_heuristics : bool; - use_hook : (env -> evar_map -> evar -> constr) option; + use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } @@ -272,7 +274,7 @@ let apply_inference_hook hook evdref pending = if Evd.is_undefined sigma evk (* in particular not defined by side-effect *) then try - let c = hook sigma evk in + let sigma, c = hook sigma evk in Evd.define evk c sigma with Exit -> sigma diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli index 824bb11aa4..eead48a549 100644 --- a/pretyping/pretyping.mli +++ b/pretyping/pretyping.mli @@ -47,10 +47,12 @@ val empty_lvar : ltac_var_map type glob_constr_ltac_closure = ltac_var_map * glob_constr type pure_open_constr = evar_map * constr +type inference_hook = env -> evar_map -> evar -> evar_map * constr + type inference_flags = { use_typeclasses : bool; use_unif_heuristics : bool; - use_hook : (env -> evar_map -> evar -> constr) option; + use_hook : inference_hook option; fail_evar : bool; expand_evars : bool } diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml index e4bae20128..a3ece19134 100644 --- a/proofs/pfedit.ml +++ b/proofs/pfedit.ml @@ -161,11 +161,12 @@ let build_constant_by_tactic id ctx sign ?(goal_kind = Global, false, Proof Theo delete_current_proof (); iraise reraise -let build_by_tactic ?(side_eff=true) env ctx ?(poly=false) typ tac = +let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac = let id = Id.of_string ("temporary_proof"^string_of_int (next())) in let sign = val_of_named_context (named_context env) in let gk = Global, poly, Proof Theorem in - let ce, status, univs = build_constant_by_tactic id ctx sign ~goal_kind:gk typ tac in + let ce, status, univs = + build_constant_by_tactic id sigma sign ~goal_kind:gk typ tac in let ce = if side_eff then Safe_typing.inline_private_constants_in_definition_entry env ce else { ce with @@ -232,8 +233,9 @@ let solve_by_implicit_tactic env sigma evk = (try let c = Evarutil.nf_evars_universes sigma evi.evar_concl in if Evarutil.has_undefined_evars sigma c then raise Exit; - let (ans, _, _) = + let (ans, _, ctx) = build_by_tactic env (Evd.evar_universe_context sigma) c tac in - ans + let sigma = Evd.set_universe_context sigma ctx in + sigma, ans with e when Logic.catchable_exception e -> raise Exit) | _ -> raise Exit diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli index 666730e1af..ea604e08eb 100644 --- a/proofs/pfedit.mli +++ b/proofs/pfedit.mli @@ -167,7 +167,8 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit val build_constant_by_tactic : Id.t -> Evd.evar_universe_context -> named_context_val -> ?goal_kind:goal_kind -> types -> unit Proofview.tactic -> - Safe_typing.private_constants Entries.definition_entry * bool * Evd.evar_universe_context + Safe_typing.private_constants Entries.definition_entry * bool * + Evd.evar_universe_context val build_by_tactic : ?side_eff:bool -> env -> Evd.evar_universe_context -> ?poly:polymorphic -> types -> unit Proofview.tactic -> @@ -189,5 +190,4 @@ val declare_implicit_tactic : unit Proofview.tactic -> unit val clear_implicit_tactic : unit -> unit (* Raise Exit if cannot solve *) -(* FIXME: interface: it may incur some new universes etc... *) -val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> constr +val solve_by_implicit_tactic : env -> Evd.evar_map -> Evd.evar -> Evd.evar_map * constr diff --git a/stm/lemmas.ml b/stm/lemmas.ml index 50f2b82c3b..022c89ad9a 100644 --- a/stm/lemmas.ml +++ b/stm/lemmas.ml @@ -449,7 +449,7 @@ let start_proof_with_initialization kind ctx recguard thms snl hook = call_hook (fun exn -> exn) hook strength ref) thms_data in start_proof_univs id ?pl kind ctx t ?init_tac (fun ctx -> mk_hook (hook ctx)) ~compute_guard:guard -let start_proof_com kind thms hook = +let start_proof_com ?inference_hook kind thms hook = let env0 = Global.env () in let levels = Option.map snd (fst (List.hd thms)) in let evdref = ref (match levels with @@ -459,7 +459,9 @@ let start_proof_com kind thms hook = let thms = List.map (fun (sopt,(bl,t,guard)) -> let impls, ((env, ctx), imps) = interp_context_evars env0 evdref bl in let t', imps' = interp_type_evars_impls ~impls env evdref t in - evdref := solve_remaining_evars all_and_fail_flags env !evdref (Evd.empty,!evdref); + let flags = all_and_fail_flags in + let flags = { flags with use_hook = inference_hook } in + evdref := solve_remaining_evars flags env !evdref (Evd.empty,!evdref); let ids = List.map get_name ctx in (compute_proof_name (pi1 kind) sopt, (nf_evar !evdref (it_mkProd_or_LetIn t' ctx), diff --git a/stm/lemmas.mli b/stm/lemmas.mli index f751598f04..39c089be9f 100644 --- a/stm/lemmas.mli +++ b/stm/lemmas.mli @@ -33,7 +33,9 @@ val start_proof_univs : Id.t -> ?pl:universe_binders -> goal_kind -> Evd.evar_ma ?init_tac:unit Proofview.tactic -> ?compute_guard:lemma_possible_guards -> (Evd.evar_universe_context option -> unit declaration_hook) -> unit -val start_proof_com : goal_kind -> Vernacexpr.proof_expr list -> +val start_proof_com : + ?inference_hook:Pretyping.inference_hook -> + goal_kind -> Vernacexpr.proof_expr list -> unit declaration_hook -> unit val start_proof_with_initialization : diff --git a/test-suite/Makefile b/test-suite/Makefile index 1dfbb29ff0..a40ea80ae4 100644 --- a/test-suite/Makefile +++ b/test-suite/Makefile @@ -304,16 +304,16 @@ $(addsuffix .log,$(wildcard output-modulo-time/*.v)): %.v.log: %.v %.out | grep -v "\[Loading ML file" \ | grep -v "Skipping rcfile loading" \ | grep -v "^<W>" \ - | sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + | sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ > $$tmpoutput; \ - sed -e 's/\s*[0-9]*\.[0-9]\+\s*//g' \ + sed -e 's/\s*[0-9]*\.[0-9][0-9]*\s*//g' \ -e 's/\s*0\.\s*//g' \ -e 's/\s*[-+]nan\s*//g' \ -e 's/\s*[-+]inf\s*//g' \ - $*.out > $$tmpexpected; \ + $*.out > $$tmpexpected; \ diff -b -u $$tmpexpected $$tmpoutput 2>&1; R=$$?; times; \ if [ $$R = 0 ]; then \ echo $(log_success); \ diff --git a/test-suite/bugs/closed/4723.v b/test-suite/bugs/closed/4723.v new file mode 100644 index 0000000000..8884812102 --- /dev/null +++ b/test-suite/bugs/closed/4723.v @@ -0,0 +1,28 @@ + +Require Coq.Program.Tactics. + +Record Matrix (m n : nat). + +Definition kp {m n p q: nat} (A: Matrix m n) (B: Matrix p q): + Matrix (m*p) (n*q). Admitted. + +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Ltac Obligation Tactic := admit. +Fail Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. + +Axiom cheat : forall {A}, A. +Obligation Tactic := apply cheat. + +Program Fact kp_assoc + (xr xc yr yc zr zc: nat) + (x: Matrix xr xc) (y: Matrix yr yc) (z: Matrix zr zc): + kp x (kp y z) = kp (kp x y) z. +admit. +Admitted.
\ No newline at end of file diff --git a/test-suite/bugs/closed/5011.v b/test-suite/bugs/closed/5011.v new file mode 100644 index 0000000000..c3043ca5d1 --- /dev/null +++ b/test-suite/bugs/closed/5011.v @@ -0,0 +1,2 @@ +Record decoder (n : nat) W := { decode : W -> nat }. +Existing Class decoder. diff --git a/test-suite/output/Arguments.v b/test-suite/output/Arguments.v index 05eeaac631..bd9240476f 100644 --- a/test-suite/output/Arguments.v +++ b/test-suite/output/Arguments.v @@ -17,7 +17,7 @@ Definition fcomp A B C f (g : A -> B) (x : A) : C := f (g x). Arguments fcomp {_ _ _}%type_scope f g x /. About fcomp. Definition volatile := fun x : nat => x. -Arguments volatile /. +Arguments volatile / _. About volatile. Set Implicit Arguments. Section S1. diff --git a/test-suite/success/simpl_tuning.v b/test-suite/success/simpl_tuning.v index d4191b939b..2728672f30 100644 --- a/test-suite/success/simpl_tuning.v +++ b/test-suite/success/simpl_tuning.v @@ -106,7 +106,7 @@ match goal with |- (f (g x1), h x2) = (f (g x1), h x2) => idtac end. Abort. Definition volatile := fun x : nat => x. -Arguments volatile /. +Arguments volatile / _. Lemma foo : volatile = volatile. simpl. diff --git a/theories/Numbers/Integer/Abstract/ZDivEucl.v b/theories/Numbers/Integer/Abstract/ZDivEucl.v index 278e1bcffa..c2fa69e535 100644 --- a/theories/Numbers/Integer/Abstract/ZDivEucl.v +++ b/theories/Numbers/Integer/Abstract/ZDivEucl.v @@ -30,18 +30,23 @@ Require Import ZAxioms ZMulOrder ZSgnAbs NZDiv. We just ignore them here. *) -Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod' A). - Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= a mod b < abs b. +Module Type EuclidSpec (Import A : ZAxiomsSig')(Import B : DivMod A). + Axiom mod_always_pos : forall a b, b ~= 0 -> 0 <= B.modulo a b < abs b. End EuclidSpec. Module Type ZEuclid (Z:ZAxiomsSig) := NZDiv.NZDiv Z <+ EuclidSpec Z. -Module Type ZEuclid' (Z:ZAxiomsSig) := NZDiv.NZDiv' Z <+ EuclidSpec Z. Module ZEuclidProp (Import A : ZAxiomsSig') (Import B : ZMulOrderProp A) (Import C : ZSgnAbsProp A B) - (Import D : ZEuclid' A). + (Import D : ZEuclid A). + + (** We put notations in a scope, to avoid warnings about + redefinitions of notations *) + Infix "/" := D.div : euclid. + Infix "mod" := D.modulo : euclid. + Local Open Scope euclid. Module Import Private_NZDiv := Nop <+ NZDivProp A D B. @@ -615,4 +620,3 @@ intros (c,Hc). rewrite Hc. now apply mod_mul. Qed. End ZEuclidProp. - diff --git a/toplevel/coqloop.ml b/toplevel/coqloop.ml index 0d4807e163..69d68bd357 100644 --- a/toplevel/coqloop.ml +++ b/toplevel/coqloop.ml @@ -348,5 +348,7 @@ let rec loop () = | any -> Feedback.msg_error (str"Anomaly: main loop exited with exception: " ++ str (Printexc.to_string any) ++ - fnl() ++ str"Please report."); + fnl() ++ + str"Please report" ++ + strbrk" at " ++ str Coq_config.wwwbugtracker ++ str "."); loop () diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index ee331e37c7..47d433d790 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -523,6 +523,7 @@ let parse_args arglist = |"-load-vernac-source-verbose"|"-lv" -> add_load_vernacular true (next ()) |"-outputstate" -> set_outputstate (next ()) |"-print-mod-uid" -> let s = String.concat " " (List.map get_native_name rem) in print_endline s; exit 0 + |"-profile-ltac-cutoff" -> Flags.profile_ltac := true; Flags.profile_ltac_cutoff := get_float opt (next ()) |"-require" -> add_require (next ()) |"-top" -> set_toplevel_name (dirpath_of_string (next ())) |"-with-geoproof" -> Coq_config.with_geoproof := get_bool opt (next ()) diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index ff4c18ad21..6ee695bc24 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -304,7 +304,8 @@ let explain_unification_error env sigma p1 p2 = function else [] | MetaOccurInBody evk -> [str "instance for " ++ quote (pr_existential_key sigma evk) ++ - strbrk " refers to a metavariable - please report your example"] + strbrk " refers to a metavariable - please report your example" ++ + strbrk "at " ++ str Coq_config.wwwbugtracker ++ str "."] | InstanceNotSameType (evk,env,t,u) -> let t, u = pr_explicit env sigma t u in [str "unable to find a well-typed instantiation for " ++ diff --git a/toplevel/record.ml b/toplevel/record.ml index 71d070776d..9c4d41ea50 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -521,11 +521,9 @@ let add_inductive_class ind = | LocalDef _ -> None | LocalAssum (_, t) -> Some (lazy t) in - let args = List.map_filter map ctx in - let ty = Inductive.type_of_inductive_knowing_parameters + let ty = Inductive.type_of_inductive (push_rel_context ctx (Global.env ())) ((mind,oneind),inst) - (Array.of_list args) in { cl_impl = IndRef ind; cl_context = List.map (const None) ctx, ctx; diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index 48a85b709f..25d16f91f5 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -448,7 +448,27 @@ let vernac_notation locality local = (***********) (* Gallina *) -let start_proof_and_print k l hook = start_proof_com k l hook +let start_proof_and_print k l hook = + let inference_hook = + if Flags.is_program_mode () then + let hook env sigma ev = + let tac = !Obligations.default_tactic in + let evi = Evd.find sigma ev in + let env = Evd.evar_filtered_env evi in + try + let concl = Evarutil.nf_evars_universes sigma evi.Evd.evar_concl in + if Evarutil.has_undefined_evars sigma concl then raise Exit; + let c, _, ctx = + Pfedit.build_by_tactic env (Evd.evar_universe_context sigma) + concl (Tacticals.New.tclCOMPLETE tac) + in Evd.set_universe_context sigma ctx, c + with Logic_monad.TacticFailure e when Logic.catchable_exception e -> + error "The statement obligations could not be resolved \ + automatically, write a statement definition first." + in Some hook + else None + in + start_proof_com ?inference_hook k l hook let no_hook = Lemmas.mk_hook (fun _ _ -> ()) @@ -986,9 +1006,9 @@ let vernac_declare_arguments locality r l nargs flags = | _::li, _::ld, _::ls -> check li ld ls | _ -> assert false in let () = match l with - | [[]] -> () + | [[]] when List.exists ((<>) `Assert) flags -> () | _ -> - List.iter2 (fun l -> check inf_names l) (names :: rest) scopes + List.iter2 (check inf_names) (names :: rest) scopes in (* we take extra scopes apart, and we check they are consistent *) let l, scopes = |