diff options
39 files changed, 930 insertions, 116 deletions
@@ -626,6 +626,9 @@ Tactics - Behavior of introduction patterns -> and <- made more uniform (hypothesis is cleared, rewrite in hypotheses and conclusion and erasing the variable when rewriting a variable). +- New experimental option "Set Standard Proposition Elimination Names" + so that case analysis or induction on schemes in Type containing + propositions now produces "H"-based names. - Tactics from plugins are now active only when the corresponding module is imported (source of incompatibilities, solvable by adding an "Import"; in the particular case of Omega, use "Require Import OmegaTactic"). @@ -1164,9 +1167,6 @@ Other tactics clears (resp. reverts) H and all the hypotheses that depend on H. - Ltac's pattern-matching now supports matching metavariables that depend on variables bound upwards in the pattern. -- New experimental option "Set Standard Proposition Elimination Names" - so that case analysis or induction on schemes in Type containing - propositions now produces "H"-based names. Tactic definitions diff --git a/doc/faq/fk.bib b/doc/faq/fk.bib index 4d90efcdb1..3410427dee 100644 --- a/doc/faq/fk.bib +++ b/doc/faq/fk.bib @@ -2171,7 +2171,7 @@ Decomposition}}, @Misc{ProofGeneral, author = {David Aspinall}, title = {Proof General}, - note = {\url{http://proofgeneral.inf.ed.ac.uk/}} + note = {\url{https://proofgeneral.github.io/}} } diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 21b72b8eff..b668239a6a 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -2280,6 +2280,15 @@ hypothesis. \end{Variants} +\optindex{Structural Injection} + +It is possible to ensure that \texttt{injection {\term}} erases the +original hypothesis and leaves the generated equalities in the context +rather than putting them as antecedents of the current goal, as if +giving \texttt{injection {\term} as} (with an empty list of names). To +obtain this behavior, the option {\tt Set Structural Injection} must +be activated. This option is off by default. + \subsection{\tt inversion \ident} \tacindex{inversion} diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index c282083b5c..10271ce0ca 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -251,7 +251,7 @@ to the \Coq\ toplevel or conversely from the \Coq\ toplevel to some files. {\ProofGeneral} is developed and distributed independently of the -system \Coq. It is freely available at \verb!proofgeneral.inf.ed.ac.uk!. +system \Coq. It is freely available at \verb!https://proofgeneral.github.io/!. \section[Module specification]{Module specification\label{gallina}\ttindex{gallina}} diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib index 70ee1f41f0..e69725838e 100644 --- a/doc/refman/biblio.bib +++ b/doc/refman/biblio.bib @@ -1199,7 +1199,7 @@ Decomposition}}, @Misc{ProofGeneral, author = {David Aspinall}, title = {Proof General}, - note = {\url{http://proofgeneral.inf.ed.ac.uk/}} + note = {\url{https://proofgeneral.github.io/}} } @Book{CoqArt, diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 7c4688f9fb..30016dedcf 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1078,12 +1078,10 @@ let sort_fields ~complete loc fields completer = match fields with | [] -> None | (first_field_ref, first_field_value):: other_fields -> - let env_error_msg = "Environment corruption for records." in - let first_field_glob_ref = - try global_reference_of_reference first_field_ref - with Not_found -> anomaly (Pp.str env_error_msg) in - let record = - try Recordops.find_projection first_field_glob_ref + let (first_field_glob_ref, record) = + try + let gr = global_reference_of_reference first_field_ref in + (gr, Recordops.find_projection gr) with Not_found -> user_err_loc (loc_of_reference first_field_ref, "intern", pr_reference first_field_ref ++ str": Not a projection") @@ -1094,7 +1092,8 @@ let sort_fields ~complete loc fields completer = let base_constructor = let global_record_id = ConstructRef record.Recordops.s_CONST in try Qualid (loc, shortest_qualid_of_global Id.Set.empty global_record_id) - with Not_found -> anomaly (Pp.str env_error_msg) in + with Not_found -> + anomaly (str "Environment corruption for records") in let (end_index, (* one past the last field index *) first_field_index, (* index of the first field of the record *) proj_list) (* list of projections *) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 931fc1ca40..1e14eeb81e 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -127,9 +127,10 @@ let type_of_global_ref gr = | Globnames.ConstructRef _ -> "constr" let remove_sections dir = - if Libnames.is_dirpath_prefix_of dir (Lib.cwd ()) then + let cwd = Lib.cwd_except_section () in + if Libnames.is_dirpath_prefix_of cwd dir then (* Not yet (fully) discharged *) - Libnames.pop_dirpath_n (Lib.sections_depth ()) (Lib.cwd ()) + cwd else (* Theorem/Lemma outside its outer section of definition *) dir diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index f96d8acc10..d2dcbd92aa 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -43,7 +43,7 @@ let is_alias_of_already_visible_name sp = function false let open_syntax_constant i ((sp,kn),(_,pat,onlyparse)) = - if not (is_alias_of_already_visible_name sp pat) then begin + if not (Int.equal i 1 && is_alias_of_already_visible_name sp pat) then begin Nametab.push_syndef (Nametab.Exactly i) sp kn; match onlyparse with | None -> diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml index a705e3004f..8d4de523a1 100644 --- a/kernel/cbytecodes.ml +++ b/kernel/cbytecodes.ml @@ -142,11 +142,29 @@ type fv = fv_elem array exception NotClosed +module Fv_elem = +struct +type t = fv_elem + +let compare e1 e2 = match e1, e2 with +| FVnamed id1, FVnamed id2 -> Id.compare id1 id2 +| FVnamed _, _ -> -1 +| FVrel _, FVnamed _ -> 1 +| FVrel r1, FVrel r2 -> Int.compare r1 r2 +| FVrel _, FVuniv_var _ -> -1 +| FVuniv_var i1, FVuniv_var i2 -> Int.compare i1 i2 +| FVuniv_var i1, _ -> 1 + +end + +module FvMap = Map.Make(Fv_elem) + (*spiwack: both type have been moved from Cbytegen because I needed then for the retroknowledge *) type vm_env = { size : int; (* longueur de la liste [n] *) - fv_rev : fv_elem list (* [fvn; ... ;fv1] *) + fv_rev : fv_elem list; (* [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (* reverse mapping *) } diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli index 6fa0841af9..5f1f09d00c 100644 --- a/kernel/cbytecodes.mli +++ b/kernel/cbytecodes.mli @@ -139,11 +139,14 @@ type fv = fv_elem array closed terms. *) exception NotClosed +module FvMap : Map.S with type key = fv_elem + (*spiwack: both type have been moved from Cbytegen because I needed them for the retroknowledge *) type vm_env = { size : int; (** length of the list [n] *) - fv_rev : fv_elem list (** [fvn; ... ;fv1] *) + fv_rev : fv_elem list; (** [fvn; ... ;fv1] *) + fv_fwd : int FvMap.t; (** reverse mapping *) } diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml index 2d1ae68f4b..008955d804 100644 --- a/kernel/cbytegen.ml +++ b/kernel/cbytegen.ml @@ -93,7 +93,12 @@ open Pre_env type argument = ArgConstr of Constr.t | ArgUniv of Univ.Level.t -let empty_fv = { size= 0; fv_rev = [] } +let empty_fv = { size= 0; fv_rev = []; fv_fwd = FvMap.empty } +let push_fv d e = { + size = e.size + 1; + fv_rev = d :: e.fv_rev; + fv_fwd = FvMap.add d e.size e.fv_fwd; +} let fv r = !(r.in_env) @@ -184,20 +189,15 @@ let push_local sz r = in_stack = (sz + 1) :: r.in_stack } (*i Compilation of variables *) -let find_at f l = - let rec aux n = function - | [] -> raise Not_found - | hd :: tl -> if f hd then n else aux (n + 1) tl - in aux 1 l +let find_at fv env = FvMap.find fv env.fv_fwd let pos_named id r = let env = !(r.in_env) in let cid = FVnamed id in - let f = function FVnamed id' -> Id.equal id id' | _ -> false in - try Kenvacc(r.offset + env.size - (find_at f env.fv_rev)) + try Kenvacc(r.offset + find_at cid env) with Not_found -> let pos = env.size in - r.in_env := { size = pos+1; fv_rev = cid:: env.fv_rev}; + r.in_env := push_fv cid env; Kenvacc (r.offset + pos) let pos_rel i r sz = @@ -212,11 +212,10 @@ let pos_rel i r sz = let i = i - r.nb_rec in let db = FVrel(i) in let env = !(r.in_env) in - let f = function FVrel j -> Int.equal i j | _ -> false in - try Kenvacc(r.offset + env.size - (find_at f env.fv_rev)) + try Kenvacc(r.offset + find_at db env) with Not_found -> let pos = env.size in - r.in_env := { size = pos+1; fv_rev = db:: env.fv_rev}; + r.in_env := push_fv db env; Kenvacc(r.offset + pos) let pos_universe_var i r sz = @@ -224,15 +223,11 @@ let pos_universe_var i r sz = Kacc (sz - r.nb_stack - (r.nb_uni_stack - i)) else let env = !(r.in_env) in - let f = function - | FVuniv_var u -> Int.equal i u - | _ -> false - in - try Kenvacc (r.offset + env.size - (find_at f env.fv_rev)) + let db = FVuniv_var i in + try Kenvacc (r.offset + find_at db env) with Not_found -> let pos = env.size in - let db = FVuniv_var i in - r.in_env := { size = pos + 1; fv_rev = db::env.fv_rev } ; + r.in_env := push_fv db env; Kenvacc(r.offset + pos) (*i Examination of the continuation *) diff --git a/lib/cMap.ml b/lib/cMap.ml index 4b058380c6..ba0873ffa7 100644 --- a/lib/cMap.ml +++ b/lib/cMap.ml @@ -34,6 +34,7 @@ sig val fold_right : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b val smartmap : ('a -> 'a) -> 'a t -> 'a t val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t + val height : 'a t -> int module Unsafe : sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t @@ -57,6 +58,7 @@ sig val fold_right : (M.t -> 'a -> 'b -> 'b) -> 'a map -> 'b -> 'b val smartmap : ('a -> 'a) -> 'a map -> 'a map val smartmapi : (M.t -> 'a -> 'a) -> 'a map -> 'a map + val height : 'a map -> int module Unsafe : sig val map : (M.t -> 'a -> M.t * 'b) -> 'a map -> 'b map @@ -168,6 +170,10 @@ struct if l == l' && r == r' && v == v' then s else map_inj (MNode (l', k, v', r', h)) + let height s = match map_prj s with + | MEmpty -> 0 + | MNode (_, _, _, _, h) -> h + module Unsafe = struct diff --git a/lib/cMap.mli b/lib/cMap.mli index 3ef7fa2c8a..2838b374ec 100644 --- a/lib/cMap.mli +++ b/lib/cMap.mli @@ -61,6 +61,9 @@ sig val smartmapi : (key -> 'a -> 'a) -> 'a t -> 'a t (** As [mapi] but tries to preserve sharing. *) + val height : 'a t -> int + (** An indication of the logarithmic size of a map *) + module Unsafe : sig val map : (key -> 'a -> key * 'b) -> 'a t -> 'b t diff --git a/lib/hMap.ml b/lib/hMap.ml index 778c366fd5..ea76e74272 100644 --- a/lib/hMap.ml +++ b/lib/hMap.ml @@ -68,34 +68,91 @@ struct Int.Map.update h m s with Not_found -> s + let height s = Int.Map.height s + + let is_smaller s1 s2 = height s1 <= height s2 + 3 + + (** Assumes s1 << s2 *) + let fast_union s1 s2 = + let fold h s accu = + try Int.Map.modify h (fun _ s' -> Set.fold Set.add s s') accu + with Not_found -> Int.Map.add h s accu + in + Int.Map.fold fold s1 s2 + let union s1 s2 = - let fu _ m1 m2 = match m1, m2 with - | None, None -> None - | (Some _ as m), None | None, (Some _ as m) -> m - | Some m1, Some m2 -> Some (Set.union m1 m2) + if is_smaller s1 s2 then fast_union s1 s2 + else if is_smaller s2 s1 then fast_union s2 s1 + else + let fu _ m1 m2 = match m1, m2 with + | None, None -> None + | (Some _ as m), None | None, (Some _ as m) -> m + | Some m1, Some m2 -> Some (Set.union m1 m2) + in + Int.Map.merge fu s1 s2 + + (** Assumes s1 << s2 *) + let fast_inter s1 s2 = + let fold h s accu = + try + let s' = Int.Map.find h s2 in + let si = Set.filter (fun e -> Set.mem e s') s in + if Set.is_empty si then accu + else Int.Map.add h si accu + with Not_found -> accu in - Int.Map.merge fu s1 s2 + Int.Map.fold fold s1 Int.Map.empty let inter s1 s2 = - let fu _ m1 m2 = match m1, m2 with - | None, None -> None - | Some _, None | None, Some _ -> None - | Some m1, Some m2 -> - let m = Set.inter m1 m2 in - if Set.is_empty m then None else Some m + if is_smaller s1 s2 then fast_inter s1 s2 + else if is_smaller s2 s1 then fast_inter s2 s1 + else + let fu _ m1 m2 = match m1, m2 with + | None, None -> None + | Some _, None | None, Some _ -> None + | Some m1, Some m2 -> + let m = Set.inter m1 m2 in + if Set.is_empty m then None else Some m + in + Int.Map.merge fu s1 s2 + + (** Assumes s1 << s2 *) + let fast_diff_l s1 s2 = + let fold h s accu = + try + let s' = Int.Map.find h s2 in + let si = Set.filter (fun e -> not (Set.mem e s')) s in + if Set.is_empty si then accu + else Int.Map.add h si accu + with Not_found -> Int.Map.add h s accu + in + Int.Map.fold fold s1 Int.Map.empty + + (** Assumes s2 << s1 *) + let fast_diff_r s1 s2 = + let fold h s accu = + try + let s' = Int.Map.find h accu in + let si = Set.filter (fun e -> not (Set.mem e s)) s' in + if Set.is_empty si then Int.Map.remove h accu + else Int.Map.update h si accu + with Not_found -> accu in - Int.Map.merge fu s1 s2 + Int.Map.fold fold s2 s1 let diff s1 s2 = - let fu _ m1 m2 = match m1, m2 with - | None, None -> None - | (Some _ as m), None -> m - | None, Some _ -> None - | Some m1, Some m2 -> - let m = Set.diff m1 m2 in - if Set.is_empty m then None else Some m - in - Int.Map.merge fu s1 s2 + if is_smaller s1 s2 then fast_diff_l s1 s2 + else if is_smaller s2 s2 then fast_diff_r s1 s2 + else + let fu _ m1 m2 = match m1, m2 with + | None, None -> None + | (Some _ as m), None -> m + | None, Some _ -> None + | Some m1, Some m2 -> + let m = Set.diff m1 m2 in + if Set.is_empty m then None else Some m + in + Int.Map.merge fu s1 s2 let compare s1 s2 = Int.Map.compare Set.compare s1 s2 @@ -324,6 +381,8 @@ struct let fs m = Map.smartmapi f m in Int.Map.smartmap fs s + let height s = Int.Map.height s + module Unsafe = struct let map f s = diff --git a/library/impargs.ml b/library/impargs.ml index 6da7e21100..bce7a15cbe 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -68,10 +68,9 @@ let is_reversible_pattern_implicit_args () = !implicit_args.reversible_pattern let is_contextual_implicit_args () = !implicit_args.contextual let is_maximal_implicit_args () = !implicit_args.maximal -let with_implicits flags f x = +let with_implicit_protection f x = let oflags = !implicit_args in try - implicit_args := flags; let rslt = f x in implicit_args := oflags; rslt diff --git a/library/impargs.mli b/library/impargs.mli index 34e529ca2c..3919a519c9 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -29,8 +29,7 @@ val is_reversible_pattern_implicit_args : unit -> bool val is_contextual_implicit_args : unit -> bool val is_maximal_implicit_args : unit -> bool -type implicits_flags -val with_implicits : implicits_flags -> ('a -> 'b) -> 'a -> 'b +val with_implicit_protection : ('a -> 'b) -> 'a -> 'b (** {6 ... } *) (** An [implicits_list] is a list of positions telling which arguments @@ -136,14 +135,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list val select_stronger_impargs : implicits_list list -> implicit_status list -type implicit_interactive_request - -type implicit_discharge_request = - | ImplLocal - | ImplConstant of constant * implicits_flags - | ImplMutualInductive of mutual_inductive * implicits_flags - | ImplInteractive of global_reference * implicits_flags * - implicit_interactive_request - val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool (** Equality on [explicitation]. *) diff --git a/ltac/ltac.mllib b/ltac/ltac.mllib index 65ed114cff..fc51e48ae4 100644 --- a/ltac/ltac.mllib +++ b/ltac/ltac.mllib @@ -1,3 +1,4 @@ +Taccoerce Tacsubst Tacenv Tactic_debug diff --git a/ltac/profile_ltac.ml b/ltac/profile_ltac.ml index bea02e3dcb..fb71becfc3 100644 --- a/ltac/profile_ltac.ml +++ b/ltac/profile_ltac.ml @@ -235,7 +235,6 @@ let rec print_node all_total indent prefix (s, n) = ++ padl 8 (string_of_int e.ncalls) ++ padl 10 (format_sec (e.max_total)) ) ++ - fnl () ++ print_table all_total indent false n.children and print_table all_total indent first_level table = diff --git a/tactics/taccoerce.ml b/ltac/taccoerce.ml index 0110510d35..0110510d35 100644 --- a/tactics/taccoerce.ml +++ b/ltac/taccoerce.ml diff --git a/tactics/taccoerce.mli b/ltac/taccoerce.mli index 0b67f8726e..0b67f8726e 100644 --- a/tactics/taccoerce.mli +++ b/ltac/taccoerce.mli diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 447a4c487c..fe2b0a5a1a 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1871,7 +1871,7 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon = (* We put the tycon inside the arity signature, possibly discovering dependencies. *) let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c = - let nar = List.fold_left (fun n sign -> List.length sign + n) 0 arsign in + let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in let subst, len = List.fold_right2 (fun (tm, tmtype) sign (subst, len) -> let signlen = List.length sign in diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 1ef96e0344..f466740036 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -403,9 +403,10 @@ let ltac_interp_name_env k0 lvar env = (* tail is the part of the env enriched by pretyping *) let n = Context.Rel.length (rel_context env) - k0 in let ctxt,_ = List.chop n (rel_context env) in - let env = pop_rel_context n env in - let ctxt = List.map (Context.Rel.Declaration.map_name (ltac_interp_name lvar)) ctxt in - push_rel_context ctxt env + let open Context.Rel.Declaration in + let ctxt' = List.smartmap (map_name (ltac_interp_name lvar)) ctxt in + if List.equal (fun d1 d2 -> Name.equal (get_name d1) (get_name d2)) ctxt ctxt' then env + else push_rel_context ctxt' (pop_rel_context n env) let invert_ltac_bound_name lvar env id0 id = let id' = Id.Map.find id lvar.ltac_idents in @@ -803,8 +804,8 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre let j = pretype_type empty_valcon env evdref lvar c2 in { j with utj_val = lift 1 j.utj_val } | Name _ -> - let var = (name,j.utj_val) in - let env' = ExtraEnv.make_env (push_rel_assum var env.ExtraEnv.env) in + let var = LocalAssum (name, j.utj_val) in + let env' = push_rel var env in pretype_type empty_valcon env' evdref lvar c2 in let name = ltac_interp_name lvar name in diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 5484e70b61..8259876c29 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -790,11 +790,11 @@ let rec whd_state_gen ?csts tactic_mode flags env sigma = (h 0 (str "<<" ++ Termops.print_constr x ++ str "|" ++ cut () ++ Cst_stack.pr cst_l ++ str "|" ++ cut () ++ Stack.pr Termops.print_constr stack ++ - str ">>") ++ fnl ()) + str ">>")) in let fold () = let () = if !debug_RAKAM then - let open Pp in Feedback.msg_notice (str "<><><><><>" ++ fnl ()) in + let open Pp in Feedback.msg_notice (str "<><><><><>") in (s,cst_l) in match kind_of_term x with diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 0c1ce0d2f8..6d80db6455 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1080,8 +1080,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb if !debug_unification then Feedback.msg_debug (str "Leaving unification with success"); a with e -> + let e = CErrors.push e in if !debug_unification then Feedback.msg_debug (str "Leaving unification with failure"); - raise e + iraise e let unify_0 env sigma = unify_0_with_initial_metas (sigma,[],[]) true env diff --git a/proofs/refiner.ml b/proofs/refiner.ml index ebd30820be..ea8543b02f 100644 --- a/proofs/refiner.ml +++ b/proofs/refiner.ml @@ -221,7 +221,7 @@ let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma) Feedback.msg_notice (str (emacs_str "<infoH>") ++ (hov 0 (str s)) - ++ (str (emacs_str "</infoH>")) ++ fnl()); + ++ (str (emacs_str "</infoH>"))); tclIDTAC goal;; diff --git a/tactics/equality.ml b/tactics/equality.ml index 2c97cf4425..3e5b7b65ff 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -629,7 +629,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt = in match evd with | None -> - tclFAIL 0 (str"Terms do not have convertible types.") + tclFAIL 0 (str"Terms do not have convertible types") | Some evd -> let e = build_coq_eq () in let sym = build_coq_eq_sym () in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 38af9a0caa..acc0fa1ca7 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1270,7 +1270,7 @@ let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) let naming = NamingMustBe (dloc,targetid) in let with_clear = do_replace (Some id) naming in Tacticals.New.tclTHEN - (Proofview.Unsafe.tclEVARS clenv.evd) + (Proofview.Unsafe.tclEVARS (clear_metas clenv.evd)) (if sidecond_first then Tacticals.New.tclTHENFIRST (assert_before_then_gen with_clear naming new_hyp_typ tac) exact_tac @@ -4865,8 +4865,13 @@ let abstract_subproof id gk tac = in let cd = Entries.DefinitionEntry const in let decl = (cd, IsProof Lemma) in - (** ppedrot: seems legit to have abstracted subproofs as local*) - let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl in + let cst () = + (** do not compute the implicit arguments, it may be costly *) + let () = Impargs.make_implicit_args false in + (** ppedrot: seems legit to have abstracted subproofs as local*) + Declare.declare_constant ~internal:Declare.InternalTacticRequest ~local:true id decl + in + let cst = Impargs.with_implicit_protection cst () in (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *) let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in let evd = Evd.set_universe_context evd ectx in diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 48722f655a..093302608e 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -12,7 +12,6 @@ Equality Contradiction Inv Leminv -Taccoerce Hints Auto Eauto diff --git a/test-suite/bugs/closed/4187.v b/test-suite/bugs/closed/4187.v new file mode 100644 index 0000000000..b13ca36a37 --- /dev/null +++ b/test-suite/bugs/closed/4187.v @@ -0,0 +1,709 @@ +(* Lifted from https://coq.inria.fr/bugs/show_bug.cgi?id=4187 *) +(* File reduced by coq-bug-finder from original input, then from 715 lines to 696 lines *) +(* coqc version 8.4pl5 (December 2014) compiled on Dec 28 2014 03:23:16 with OCaml 4.01.0 + coqtop version 8.4pl5 (December 2014) *) +Set Asymmetric Patterns. +Axiom proof_admitted : False. +Tactic Notation "admit" := case proof_admitted. +Require Import Coq.Lists.List. +Require Import Coq.Setoids.Setoid. +Require Import Coq.Numbers.Natural.Peano.NPeano. +Global Set Implicit Arguments. +Global Generalizable All Variables. +Coercion is_true : bool >-> Sortclass. +Coercion bool_of_sumbool {A B} (x : {A} + {B}) : bool := if x then true else false. +Fixpoint ForallT {T} (P : T -> Type) (ls : list T) : Type + := match ls return Type with + | nil => True + | x::xs => (P x * ForallT P xs)%type + end. +Fixpoint Forall_tails {T} (P : list T -> Type) (ls : list T) : Type + := match ls with + | nil => P nil + | x::xs => (P (x::xs) * Forall_tails P xs)%type + end. + +Module Export ADTSynthesis_DOT_Common_DOT_Wf. +Module Export ADTSynthesis. +Module Export Common. +Module Export Wf. + +Section wf. + Section wf_prod. + Context A B (RA : relation A) (RB : relation B). +Definition prod_relation : relation (A * B). +exact (fun ab a'b' => + RA (fst ab) (fst a'b') \/ (fst a'b' = fst ab /\ RB (snd ab) (snd a'b'))). +Defined. + + Fixpoint well_founded_prod_relation_helper + a b + (wf_A : Acc RA a) (wf_B : well_founded RB) {struct wf_A} + : Acc prod_relation (a, b) + := match wf_A with + | Acc_intro fa => (fix wf_B_rec b' (wf_B' : Acc RB b') : Acc prod_relation (a, b') + := Acc_intro + _ + (fun ab => + match ab as ab return prod_relation ab (a, b') -> Acc prod_relation ab with + | (a'', b'') => + fun pf => + match pf with + | or_introl pf' + => @well_founded_prod_relation_helper + _ _ + (fa _ pf') + wf_B + | or_intror (conj pfa pfb) + => match wf_B' with + | Acc_intro fb + => eq_rect + _ + (fun a'' => Acc prod_relation (a'', b'')) + (wf_B_rec _ (fb _ pfb)) + _ + pfa + end + end + end) + ) b (wf_B b) + end. + + Definition well_founded_prod_relation : well_founded RA -> well_founded RB -> well_founded prod_relation. + Proof. + intros wf_A wf_B [a b]; hnf in *. + apply well_founded_prod_relation_helper; auto. + Defined. + End wf_prod. + + Section wf_projT1. + Context A (B : A -> Type) (R : relation A). +Definition projT1_relation : relation (sigT B). +exact (fun ab a'b' => + R (projT1 ab) (projT1 a'b')). +Defined. + + Definition well_founded_projT1_relation : well_founded R -> well_founded projT1_relation. + Proof. + intros wf [a b]; hnf in *. + induction (wf a) as [a H IH]. + constructor. + intros y r. + specialize (IH _ r (projT2 y)). + destruct y. + exact IH. + Defined. + End wf_projT1. +End wf. + +Section Fix3. + Context A (B : A -> Type) (C : forall a, B a -> Type) (D : forall a b, C a b -> Type) + (R : A -> A -> Prop) (Rwf : well_founded R) + (P : forall a b c, D a b c -> Type) + (F : forall x : A, (forall y : A, R y x -> forall b c d, P y b c d) -> forall b c d, P x b c d). +Definition Fix3 a b c d : @P a b c d. +exact (@Fix { a : A & { b : B a & { c : C b & D c } } } + (fun x y => R (projT1 x) (projT1 y)) + (well_founded_projT1_relation Rwf) + (fun abcd => P (projT2 (projT2 (projT2 abcd)))) + (fun x f => @F (projT1 x) (fun y r b c d => f (existT _ y (existT _ b (existT _ c d))) r) _ _ _) + (existT _ a (existT _ b (existT _ c d)))). +Defined. +End Fix3. + +End Wf. + +End Common. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Common_DOT_Wf. + +Module Export ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. +Module Export ADTSynthesis. +Module Export Parsers. +Module Export StringLike. +Module Export Core. +Import Coq.Setoids.Setoid. +Import Coq.Classes.Morphisms. + + + +Module Export StringLike. + Class StringLike {Char : Type} := + { + String :> Type; + is_char : String -> Char -> bool; + length : String -> nat; + take : nat -> String -> String; + drop : nat -> String -> String; + bool_eq : String -> String -> bool; + beq : relation String := fun x y => bool_eq x y + }. + + Arguments StringLike : clear implicits. + Infix "=s" := (@beq _ _) (at level 70, no associativity) : type_scope. + Notation "s ~= [ ch ]" := (is_char s ch) (at level 70, no associativity) : string_like_scope. + Local Open Scope string_like_scope. + + Definition str_le `{StringLike Char} (s1 s2 : String) + := length s1 < length s2 \/ s1 =s s2. + Infix "≤s" := str_le (at level 70, right associativity). + + Class StringLikeProperties (Char : Type) `{StringLike Char} := + { + singleton_unique : forall s ch ch', s ~= [ ch ] -> s ~= [ ch' ] -> ch = ch'; + length_singleton : forall s ch, s ~= [ ch ] -> length s = 1; + bool_eq_char : forall s s' ch, s ~= [ ch ] -> s' ~= [ ch ] -> s =s s'; + is_char_Proper :> Proper (beq ==> eq ==> eq) is_char; + length_Proper :> Proper (beq ==> eq) length; + take_Proper :> Proper (eq ==> beq ==> beq) take; + drop_Proper :> Proper (eq ==> beq ==> beq) drop; + bool_eq_Equivalence :> Equivalence beq; + bool_eq_empty : forall str str', length str = 0 -> length str' = 0 -> str =s str'; + take_short_length : forall str n, n <= length str -> length (take n str) = n; + take_long : forall str n, length str <= n -> take n str =s str; + take_take : forall str n m, take n (take m str) =s take (min n m) str; + drop_length : forall str n, length (drop n str) = length str - n; + drop_0 : forall str, drop 0 str =s str; + drop_drop : forall str n m, drop n (drop m str) =s drop (n + m) str; + drop_take : forall str n m, drop n (take m str) =s take (m - n) (drop n str); + take_drop : forall str n m, take n (drop m str) =s drop m (take (n + m) str) + }. + + Arguments StringLikeProperties Char {_}. +End StringLike. + +End Core. + +End StringLike. + +End Parsers. + +End ADTSynthesis. + +End ADTSynthesis_DOT_Parsers_DOT_StringLike_DOT_Core. + +Module Export ADTSynthesis. +Module Export Parsers. +Module Export ContextFreeGrammar. +Require Import Coq.Strings.String. +Require Import Coq.Lists.List. +Export ADTSynthesis.Parsers.StringLike.Core. +Import ADTSynthesis.Common. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char : Type}. + + Section definitions. + + Inductive item := + | Terminal (_ : Char) + | NonTerminal (_ : string). + + Definition production := list item. + Definition productions := list production. + + Record grammar := + { + Start_symbol :> string; + Lookup :> string -> productions; + Start_productions :> productions := Lookup Start_symbol; + Valid_nonterminals : list string; + Valid_productions : list productions := map Lookup Valid_nonterminals + }. + End definitions. + + Section parse. + Context {HSL : StringLike Char}. + Variable G : grammar. + + Inductive parse_of (str : String) : productions -> Type := + | ParseHead : forall pat pats, parse_of_production str pat + -> parse_of str (pat::pats) + | ParseTail : forall pat pats, parse_of str pats + -> parse_of str (pat::pats) + with parse_of_production (str : String) : production -> Type := + | ParseProductionNil : length str = 0 -> parse_of_production str nil + | ParseProductionCons : forall n pat pats, + parse_of_item (take n str) pat + -> parse_of_production (drop n str) pats + -> parse_of_production str (pat::pats) + with parse_of_item (str : String) : item -> Type := + | ParseTerminal : forall ch, str ~= [ ch ] -> parse_of_item str (Terminal ch) + | ParseNonTerminal : forall nt, parse_of str (Lookup G nt) + -> parse_of_item str (NonTerminal nt). + End parse. +End cfg. + +Arguments item _ : clear implicits. +Arguments production _ : clear implicits. +Arguments productions _ : clear implicits. +Arguments grammar _ : clear implicits. + +End ContextFreeGrammar. + +Module Export BaseTypes. + +Section recursive_descent_parser. + + Class parser_computational_predataT := + { nonterminals_listT : Type; + initial_nonterminals_data : nonterminals_listT; + is_valid_nonterminal : nonterminals_listT -> String.string -> bool; + remove_nonterminal : nonterminals_listT -> String.string -> nonterminals_listT; + nonterminals_listT_R : nonterminals_listT -> nonterminals_listT -> Prop; + remove_nonterminal_dec : forall ls nonterminal, + is_valid_nonterminal ls nonterminal + -> nonterminals_listT_R (remove_nonterminal ls nonterminal) ls; + ntl_wf : well_founded nonterminals_listT_R }. + + Class parser_removal_dataT' `{predata : parser_computational_predataT} := + { remove_nonterminal_1 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' + -> is_valid_nonterminal ls ps'; + remove_nonterminal_2 + : forall ls ps ps', + is_valid_nonterminal (remove_nonterminal ls ps) ps' = false + <-> is_valid_nonterminal ls ps' = false \/ ps = ps' }. +End recursive_descent_parser. + +End BaseTypes. +Import Coq.Lists.List. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Local Open Scope string_like_scope. + +Section cfg. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + Context {predata : @parser_computational_predataT} + {rdata' : @parser_removal_dataT' predata}. + + Inductive minimal_parse_of + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + productions Char -> Type := + | MinParseHead : forall str0 valid str pat pats, + @minimal_parse_of_production str0 valid str pat + -> @minimal_parse_of str0 valid str (pat::pats) + | MinParseTail : forall str0 valid str pat pats, + @minimal_parse_of str0 valid str pats + -> @minimal_parse_of str0 valid str (pat::pats) + with minimal_parse_of_production + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + production Char -> Type := + | MinParseProductionNil : forall str0 valid str, + length str = 0 + -> @minimal_parse_of_production str0 valid str nil + | MinParseProductionCons : forall str0 valid str n pat pats, + str ≤s str0 + -> @minimal_parse_of_item str0 valid (take n str) pat + -> @minimal_parse_of_production str0 valid (drop n str) pats + -> @minimal_parse_of_production str0 valid str (pat::pats) + with minimal_parse_of_item + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + item Char -> Type := + | MinParseTerminal : forall str0 valid str ch, + str ~= [ ch ] + -> @minimal_parse_of_item str0 valid str (Terminal ch) + | MinParseNonTerminal + : forall str0 valid str (nt : String.string), + @minimal_parse_of_nonterminal str0 valid str nt + -> @minimal_parse_of_item str0 valid str (NonTerminal nt) + with minimal_parse_of_nonterminal + : forall (str0 : String) (valid : nonterminals_listT) + (str : String), + String.string -> Type := + | MinParseNonTerminalStrLt + : forall str0 valid (nt : String.string) str, + length str < length str0 + -> is_valid_nonterminal initial_nonterminals_data nt + -> @minimal_parse_of str initial_nonterminals_data str (Lookup G nt) + -> @minimal_parse_of_nonterminal str0 valid str nt + | MinParseNonTerminalStrEq + : forall str0 str valid nonterminal, + str =s str0 + -> is_valid_nonterminal initial_nonterminals_data nonterminal + -> is_valid_nonterminal valid nonterminal + -> @minimal_parse_of str0 (remove_nonterminal valid nonterminal) str (Lookup G nonterminal) + -> @minimal_parse_of_nonterminal str0 valid str nonterminal. +End cfg. +Import ADTSynthesis.Common. + +Section general. + Context {Char} {HSL : StringLike Char} {G : grammar Char}. + + Class boolean_parser_dataT := + { predata :> parser_computational_predataT; + split_string_for_production + : item Char -> production Char -> String -> list nat }. + + Global Coercion predata : boolean_parser_dataT >-> parser_computational_predataT. + + Definition split_list_completeT `{data : @parser_computational_predataT} + {str0 valid} + (it : item Char) (its : production Char) + (str : String) + (pf : str ≤s str0) + (split_list : list nat) + + := ({ n : nat + & (minimal_parse_of_item (G := G) (predata := data) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type) + -> ({ n : nat + & (In n split_list) + * (minimal_parse_of_item (G := G) str0 valid (take n str) it) + * (minimal_parse_of_production (G := G) str0 valid (drop n str) its) }%type). + + Class boolean_parser_completeness_dataT' `{data : boolean_parser_dataT} := + { split_string_for_production_complete + : forall str0 valid str (pf : str ≤s str0) nt, + is_valid_nonterminal initial_nonterminals_data nt + -> ForallT + (Forall_tails + (fun prod + => match prod return Type with + | nil => True + | it::its + => @split_list_completeT data str0 valid it its str pf (split_string_for_production it its str) + end)) + (Lookup G nt) }. +End general. + +Module Export BooleanRecognizer. +Import Coq.Numbers.Natural.Peano.NPeano. +Import Coq.Arith.Compare_dec. +Import Coq.Arith.Wf_nat. + +Section recursive_descent_parser. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} {G : grammar Char}. + Context {data : @boolean_parser_dataT Char _}. + + Section bool. + Section parts. +Definition parse_item + (str_matches_nonterminal : String.string -> bool) + (str : String) + (it : item Char) + : bool. +Admitted. + + Section production. + Context {str0} + (parse_nonterminal + : forall (str : String), + str ≤s str0 + -> String.string + -> bool). + + Fixpoint parse_production + (str : String) + (pf : str ≤s str0) + (prod : production Char) + : bool. + Proof. + refine + match prod with + | nil => + + Nat.eq_dec (length str) 0 + | it::its + => let parse_production' := fun str pf => parse_production str pf its in + fold_right + orb + false + (map (fun n => + (parse_item + (parse_nonterminal (str := take n str) _) + (take n str) + it) + && parse_production' (drop n str) _)%bool + (split_string_for_production it its str)) + end; + revert pf; clear -HSLP; intros; admit. + Defined. + End production. + + Section productions. + Context {str0} + (parse_nonterminal + : forall (str : String) + (pf : str ≤s str0), + String.string -> bool). +Definition parse_productions + (str : String) + (pf : str ≤s str0) + (prods : productions Char) + : bool. +exact (fold_right orb + false + (map (parse_production parse_nonterminal pf) + prods)). +Defined. + End productions. + + Section nonterminals. + Section step. + Context {str0 valid} + (parse_nonterminal + : forall (p : String * nonterminals_listT), + prod_relation (ltof _ length) nonterminals_listT_R p (str0, valid) + -> forall str : String, + str ≤s fst p -> String.string -> bool). + + Definition parse_nonterminal_step + (str : String) + (pf : str ≤s str0) + (nt : String.string) + : bool. + Proof. + refine + (if lt_dec (length str) (length str0) + then + parse_productions + (@parse_nonterminal + (str : String, initial_nonterminals_data) + (or_introl _)) + (or_intror (reflexivity _)) + (Lookup G nt) + else + if Sumbool.sumbool_of_bool (is_valid_nonterminal valid nt) + then + parse_productions + (@parse_nonterminal + (str0 : String, remove_nonterminal valid nt) + (or_intror (conj eq_refl (remove_nonterminal_dec _ nt _)))) + (str := str) + _ + (Lookup G nt) + else + false); + assumption. + Defined. + End step. + + Section wf. +Definition parse_nonterminal_or_abort + : forall (p : String * nonterminals_listT) + (str : String), + str ≤s fst p + -> String.string + -> bool. +exact (Fix3 + _ _ _ + (well_founded_prod_relation + (well_founded_ltof _ length) + ntl_wf) + _ + (fun sl => @parse_nonterminal_step (fst sl) (snd sl))). +Defined. +Definition parse_nonterminal + (str : String) + (nt : String.string) + : bool. +exact (@parse_nonterminal_or_abort + (str : String, initial_nonterminals_data) str + (or_intror (reflexivity _)) nt). +Defined. + End wf. + End nonterminals. + End parts. + End bool. +End recursive_descent_parser. + +Section cfg. + Context {Char} {HSL : StringLike Char} {HSLP : @StringLikeProperties Char HSL} (G : grammar Char). + + Section definitions. + Context (P : String -> String.string -> Type). + + Definition Forall_parse_of_item' + (Forall_parse_of : forall {str pats} (p : parse_of G str pats), Type) + {str it} (p : parse_of_item G str it) + := match p return Type with + | ParseTerminal ch pf => unit + | ParseNonTerminal nt p' + => (P str nt * Forall_parse_of p')%type + end. + + Fixpoint Forall_parse_of {str pats} (p : parse_of G str pats) + := match p with + | ParseHead pat pats p' + => Forall_parse_of_production p' + | ParseTail _ _ p' + => Forall_parse_of p' + end + with Forall_parse_of_production {str pat} (p : parse_of_production G str pat) + := match p return Type with + | ParseProductionNil pf => unit + | ParseProductionCons pat strs pats p' p'' + => (Forall_parse_of_item' (@Forall_parse_of) p' * Forall_parse_of_production p'')%type + end. + + Definition Forall_parse_of_item {str it} (p : parse_of_item G str it) + := @Forall_parse_of_item' (@Forall_parse_of) str it p. + End definitions. + + End cfg. + +Section recursive_descent_parser_list. + Context {Char} {HSL : StringLike Char} {HLSP : StringLikeProperties Char} {G : grammar Char}. +Definition rdp_list_nonterminals_listT : Type. +exact (list String.string). +Defined. +Definition rdp_list_is_valid_nonterminal : rdp_list_nonterminals_listT -> String.string -> bool. +admit. +Defined. +Definition rdp_list_remove_nonterminal : rdp_list_nonterminals_listT -> String.string -> rdp_list_nonterminals_listT. +admit. +Defined. +Definition rdp_list_nonterminals_listT_R : rdp_list_nonterminals_listT -> rdp_list_nonterminals_listT -> Prop. +exact (ltof _ (@List.length _)). +Defined. + Lemma rdp_list_remove_nonterminal_dec : forall ls prods, + @rdp_list_is_valid_nonterminal ls prods = true + -> @rdp_list_nonterminals_listT_R (@rdp_list_remove_nonterminal ls prods) ls. +admit. +Defined. + Lemma rdp_list_ntl_wf : well_founded rdp_list_nonterminals_listT_R. + Proof. + unfold rdp_list_nonterminals_listT_R. + intro. + apply well_founded_ltof. + Defined. + + Global Instance rdp_list_predata : parser_computational_predataT + := { nonterminals_listT := rdp_list_nonterminals_listT; + initial_nonterminals_data := Valid_nonterminals G; + is_valid_nonterminal := rdp_list_is_valid_nonterminal; + remove_nonterminal := rdp_list_remove_nonterminal; + nonterminals_listT_R := rdp_list_nonterminals_listT_R; + remove_nonterminal_dec := rdp_list_remove_nonterminal_dec; + ntl_wf := rdp_list_ntl_wf }. +End recursive_descent_parser_list. + +Section sound. + Section general. + Context {Char} {HSL : StringLike Char} {HSLP : StringLikeProperties Char} (G : grammar Char). + Context {data : @boolean_parser_dataT Char _} + {cdata : @boolean_parser_completeness_dataT' Char _ G data} + {rdata : @parser_removal_dataT' predata}. + + Section parts. + + Section nonterminals. + Section wf. + + Lemma parse_nonterminal_sound + (str : String) (nonterminal : String.string) + : parse_nonterminal (G := G) str nonterminal + = true + -> parse_of_item G str (NonTerminal nonterminal). +admit. +Defined. + End wf. + End nonterminals. + End parts. + End general. +End sound. + +Import Coq.Strings.String. +Import ADTSynthesis.Parsers.ContextFreeGrammar. + +Fixpoint list_to_productions {T} (default : T) (ls : list (string * T)) : string -> T + := match ls with + | nil => fun _ => default + | (str, t)::ls' => fun s => if string_dec str s + then t + else list_to_productions default ls' s + end. + +Fixpoint list_to_grammar {T} (default : productions T) (ls : list (string * productions T)) : grammar T + := {| Start_symbol := hd ""%string (map (@fst _ _) ls); + Lookup := list_to_productions default ls; + Valid_nonterminals := map (@fst _ _) ls |}. + +Section interface. + Context {Char} (G : grammar Char). +Definition production_is_reachable (p : production Char) : Prop. +admit. +Defined. +Definition split_list_is_complete `{HSL : StringLike Char} (str : String) (it : item Char) (its : production Char) + (splits : list nat) + : Prop. +exact (forall n, + n <= length str + -> parse_of_item G (take n str) it + -> parse_of_production G (drop n str) its + -> production_is_reachable (it::its) + -> List.In n splits). +Defined. + + Record Splitter := + { + string_type :> StringLike Char; + splits_for : String -> item Char -> production Char -> list nat; + + string_type_properties :> StringLikeProperties Char; + splits_for_complete : forall str it its, + split_list_is_complete str it its (splits_for str it its) + + }. + Global Existing Instance string_type_properties. + + Record Parser (HSL : StringLike Char) := + { + has_parse : @String Char HSL -> bool; + + has_parse_sound : forall str, + has_parse str = true + -> parse_of_item G str (NonTerminal (Start_symbol G)); + + has_parse_complete : forall str (p : parse_of_item G str (NonTerminal (Start_symbol G))), + Forall_parse_of_item + (fun _ nt => List.In nt (Valid_nonterminals G)) + p + -> has_parse str = true + }. +End interface. + +Module Export ParserImplementation. + +Section implementation. + Context {Char} {G : grammar Char}. + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := + { predata := rdp_list_predata (G := G); + split_string_for_production it its str + := splits_for splitter str it its }. + + Program Definition parser : Parser G splitter + := {| has_parse str := parse_nonterminal (G := G) (data := parser_data) str (Start_symbol G); + has_parse_sound str Hparse := parse_nonterminal_sound G _ _ Hparse; + has_parse_complete str p Hp := _ |}. + Next Obligation. +admit. +Defined. +End implementation. + +End ParserImplementation. + +Section implementation. + Context {Char} {ls : list (String.string * productions Char)}. + Local Notation G := (list_to_grammar (nil::nil) ls) (only parsing). + Context (splitter : Splitter G). + + Local Instance parser_data : @boolean_parser_dataT Char _ := parser_data splitter. + + Goal forall str : @String Char splitter, + let G' := + @BooleanRecognizer.parse_nonterminal Char splitter splitter G parser_data str G = true in + G'. + intros str G'. + Timeout 1 assert (pf' : G' -> Prop) by abstract admit. diff --git a/test-suite/bugs/closed/4904.v b/test-suite/bugs/closed/4904.v new file mode 100644 index 0000000000..a47c3b07a9 --- /dev/null +++ b/test-suite/bugs/closed/4904.v @@ -0,0 +1,11 @@ +Module A. +Module B. +Notation mynat := nat. +Notation nat := nat. +End B. +End A. + +Print A.B.nat. (* Notation A.B.nat := nat *) +Import A. +Print B.mynat. +Print B.nat. diff --git a/test-suite/success/Case13.v b/test-suite/success/Case13.v index f14725a8ee..8f95484cfd 100644 --- a/test-suite/success/Case13.v +++ b/test-suite/success/Case13.v @@ -55,6 +55,14 @@ Check (fun x : I' 0 => match x with | _ => 0 end). +(* This one could eventually be solved, the "Fail" is just to ensure *) +(* that it does not fail with an anomaly, as it did at some time *) +Fail Check (fun x : I' 0 => match x return _ x with + | C2' _ _ => 0 + | niln => 0 + | _ => 0 + end). + (* Check insertion of coercions around matched subterm *) Parameter A:Set. diff --git a/test-suite/success/programequality.v b/test-suite/success/programequality.v new file mode 100644 index 0000000000..414c572f81 --- /dev/null +++ b/test-suite/success/programequality.v @@ -0,0 +1,13 @@ +Require Import Program. + +Axiom t : nat -> Set. + +Goal forall (x y : nat) (e : x = y) (e' : x = y) (P : t y -> x = y -> Type) + (a : t x), + P (eq_rect _ _ a _ e) e'. +Proof. + intros. + pi_eq_proofs. clear e. + destruct e'. simpl. + change (P a eq_refl). +Abort.
\ No newline at end of file diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index a349eb9085..d6f9bb9df0 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -8,7 +8,6 @@ (** Tactics related to (dependent) equality and proof irrelevance. *) -Require Export ProofIrrelevance. Require Export JMeq. Require Import Coq.Program.Tactics. @@ -143,7 +142,7 @@ Ltac pi_eq_proof_hyp p := | [ H : X = Y |- _ ] => match p with | H => fail 2 - | _ => rewrite (proof_irrelevance (X = Y) p H) + | _ => rewrite (UIP _ X Y p H) end | _ => fail " No hypothesis with same type " end @@ -166,7 +165,7 @@ Hint Rewrite <- eq_rect_eq : refl_id. [coerce_* t eq_refl = t]. *) Lemma JMeq_eq_refl {A} (x : A) : JMeq_eq (@JMeq_refl _ x) = eq_refl. -Proof. apply proof_irrelevance. Qed. +Proof. apply UIP. Qed. Lemma UIP_refl_refl A (x : A) : Eqdep.EqdepTheory.UIP_refl A x eq_refl = eq_refl. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index c8f37318d1..2a3ec926b2 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -9,6 +9,7 @@ Require Import Coq.Program.Utils. Require Import Coq.Program.Equality. +Require Export ProofIrrelevance. Local Open Scope program_scope. diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll index 005ffdae72..919f37b91b 100644 --- a/tools/coqdoc/cpretty.mll +++ b/tools/coqdoc/cpretty.mll @@ -675,7 +675,7 @@ and doc_bol = parse in match check_start_list line with | Neither -> backtrack_past_newline lexbuf; doc None lexbuf - | List n -> Output.paragraph (); + | List n -> if lines > 0 then Output.paragraph (); Output.item 1; doc (Some [n]) lexbuf | Rule -> Output.rule (); doc None lexbuf } @@ -736,24 +736,7 @@ and doc_list_bol indents = parse in let (n_spaces,_) = count_spaces buf in match find_level indents n_spaces with - | InLevel _ -> - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - | StartLevel n -> - if n = 1 then - begin - Output.stop_item (); - backtrack_past_newline lexbuf; - doc_bol lexbuf - end - else - begin - Output.paragraph (); - backtrack_past_newline lexbuf; - doc_list_bol indents lexbuf - end - | Before -> + | StartLevel 1 | Before -> (* Here we were at the beginning of a line, and it was blank. The next line started before any list items. So: insert a paragraph for the empty line, rewind to whatever's just @@ -763,6 +746,10 @@ and doc_list_bol indents = parse Output.paragraph (); backtrack_past_newline lexbuf; doc_bol lexbuf + | StartLevel _ | InLevel _ -> + Output.paragraph (); + backtrack_past_newline lexbuf; + doc_list_bol indents lexbuf } | space* _ @@ -771,10 +758,7 @@ and doc_list_bol indents = parse | Before -> Output.stop_item (); backtrack lexbuf; doc_bol lexbuf | StartLevel n -> - (if n = 1 then - Output.stop_item () - else - Output.reach_item_level (n-1)); + Output.reach_item_level (n-1); backtrack lexbuf; doc (Some (take (n-1) indents)) lexbuf | InLevel (n,_) -> diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index c49a97cadb..a56459f180 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -382,7 +382,7 @@ let get_host_port opt s = Some (Spawned.Socket(host, int_of_string portr, int_of_string portw)) | ["stdfds"] -> Some Spawned.AnonPipe | _ -> - prerr_endline ("Error: host:port or stdfds expected after option "^opt); + prerr_endline ("Error: host:portr:portw or stdfds expected after option "^opt); exit 1 let get_error_resilience opt = function diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index b3eae3765b..ff4c18ad21 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -320,6 +320,7 @@ let explain_unification_error env sigma p1 p2 = function | CannotSolveConstraint ((pb,env,t,u),e) -> let t = Evarutil.nf_evar sigma t in let u = Evarutil.nf_evar sigma u in + let env = make_all_name_different env in (strbrk "cannot satisfy constraint " ++ pr_lconstr_env env sigma t ++ str " == " ++ pr_lconstr_env env sigma u) :: aux t u e diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index b4926cf786..6dba2c51ea 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -101,7 +101,7 @@ let verbose_phrase verbch loc = let s = String.create len in seek_in ch (fst loc); really_input ch s 0 len; - Feedback.msg_notice (str s ++ fnl ()) + Feedback.msg_notice (str s) | None -> () exception End_of_input diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index f69c4fa186..f87fa8a447 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -1064,7 +1064,7 @@ let vernac_declare_arguments locality r l nargs flags = vernac_declare_implicits locality r [] else if some_implicits_specified || List.mem `ClearImplicits flags then vernac_declare_implicits locality r implicits; - if nargs >= 0 && nargs < List.fold_left max 0 rargs then + if nargs >= 0 && nargs <= List.fold_left max ~-1 rargs then error "The \"/\" option must be placed after the last \"!\"."; let no_flags = List.is_empty flags in let rec narrow = function |