From 745c5325d79e754faecd0e1db75744f436f61a3b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 1 Sep 2016 21:59:17 +0200 Subject: Typo. --- tactics/tactics.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f47141efb..8dfb52632 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -1475,7 +1475,7 @@ let default_elim with_evars clear_flag (c,_ as cx) = begin function (e, info) -> match e with | IsNonrec -> (* For records, induction principles aren't there by default - anymore. Instead, we do a case analysis instead. *) + anymore. Instead, we do a case analysis. *) general_case_analysis with_evars clear_flag cx | e -> Proofview.tclZERO ~info e end -- cgit v1.2.3 From ccbb78b17fada5d9f0f5937dc276cb0b0960f4c3 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Sep 2016 18:27:58 +0200 Subject: Continuing fix to #5078, taking also into account intropatterns. Getting closer from before when the bug was introduced + test. --- ltac/taccoerce.ml | 11 ++++++----- test-suite/bugs/closed/5078.v | 5 +++++ 2 files changed, 11 insertions(+), 5 deletions(-) create mode 100644 test-suite/bugs/closed/5078.v diff --git a/ltac/taccoerce.ml b/ltac/taccoerce.ml index 46469df6a..b0a80ef73 100644 --- a/ltac/taccoerce.ml +++ b/ltac/taccoerce.ml @@ -236,13 +236,15 @@ let coerce_to_closed_constr env v = let coerce_to_evaluable_ref env v = let fail () = raise (CannotCoerceTo "an evaluable reference") in let v = Value.normalize v in + let ev = if has_type v (topwit wit_intro_pattern) then match out_gen (topwit wit_intro_pattern) v with | _, IntroNaming (IntroIdentifier id) when is_variable env id -> EvalVarRef id | _ -> fail () else if has_type v (topwit wit_var) then - let ev = EvalVarRef (out_gen (topwit wit_var) v) in - if Tacred.is_evaluable env ev then ev else fail () + let id = out_gen (topwit wit_var) v in + if Id.List.mem id (Termops.ids_of_context env) then EvalVarRef id + else fail () else if has_type v (topwit wit_ref) then let open Globnames in let r = out_gen (topwit wit_ref) v in @@ -251,12 +253,11 @@ let coerce_to_evaluable_ref env v = | ConstRef c -> EvalConstRef c | IndRef _ | ConstructRef _ -> fail () else - let ev = match Value.to_constr v with + match Value.to_constr v with | Some c when isConst c -> EvalConstRef (Univ.out_punivs (destConst c)) | Some c when isVar c -> EvalVarRef (destVar c) | _ -> fail () - in - if Tacred.is_evaluable env ev then ev else fail () + in if Tacred.is_evaluable env ev then ev else fail () let coerce_to_constr_list env v = let v = Value.to_list v in diff --git a/test-suite/bugs/closed/5078.v b/test-suite/bugs/closed/5078.v new file mode 100644 index 000000000..ca73cbcc1 --- /dev/null +++ b/test-suite/bugs/closed/5078.v @@ -0,0 +1,5 @@ +(* Test coercion from ident to evaluable reference *) +Tactic Notation "unfold_hyp" hyp(H) := cbv delta [H]. +Goal True -> Type. + intro H''. + Fail unfold_hyp H''. -- cgit v1.2.3 From 6eede071cb97e1e39772c2bdecb5189c4fa2adb0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 21 Jan 2016 23:28:40 +0100 Subject: Extending "contradiction" so that it recognizes statements such as "~x=x" or ~True. Found 1 incompatibility in tested contribs and 3 times the same pattern of incompatibility in the standard library. In all cases, it is an improvement in the form of the script. New behavior deactivated when version is <= 8.5. --- CHANGES | 4 ++++ doc/refman/RefMan-tac.tex | 8 ++++---- tactics/contradiction.ml | 17 +++++++++++++++++ theories/Numbers/Integer/BigZ/ZMake.v | 2 +- theories/Numbers/Natural/BigN/NMake.v | 2 +- theories/Structures/OrdersFacts.v | 2 +- 6 files changed, 28 insertions(+), 7 deletions(-) diff --git a/CHANGES b/CHANGES index 594bbc831..f7e1dee4c 100644 --- a/CHANGES +++ b/CHANGES @@ -61,6 +61,10 @@ Tactics "Structural Injection". In this case, hypotheses are also put in the context in the natural left-to-right order and the hypothesis on which injection applies is cleared. +- Tactic "contradiction" (hence "easy") now also solve goals with + hypotheses of the form "~True" or "t<>t" (possible source of + incompatibilities because of more successes in automation, but + generally a more intuitive strategy). Hints diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 8172b5771..65b49893b 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -1491,10 +1491,10 @@ the local context. \tacindex{contradiction} This tactic applies to any goal. The {\tt contradiction} tactic -attempts to find in the current context (after all {\tt intros}) one -hypothesis that is equivalent to {\tt False}. It permits to prune -irrelevant cases. This tactic is a macro for the tactics sequence -{\tt intros; elimtype False; assumption}. +attempts to find in the current context (after all {\tt intros}) an +hypothesis that is equivalent to an empty inductive type (e.g. {\tt + False}), to the negation of a singleton inductive type (e.g. {\tt + True} or {\tt x=x}), or two contradictory hypotheses. \begin{ErrMsgs} \item \errindex{No such assumption} diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml index c3796b484..445a104d6 100644 --- a/tactics/contradiction.ml +++ b/tactics/contradiction.ml @@ -42,6 +42,8 @@ let absurd c = absurd c (* Contradiction *) +let use_negated_unit_or_eq_type () = Flags.version_strictly_greater Flags.V8_5 + (** [f] does not assume its argument to be [nf_evar]-ed. *) let filter_hyp f tac = let rec seek = function @@ -67,6 +69,21 @@ let contradiction_context = simplest_elim (mkVar id) else match kind_of_term typ with | Prod (na,t,u) when is_empty_type u -> + let is_unit_or_eq = + if use_negated_unit_or_eq_type () then match_with_unit_or_eq_type t + else None in + Tacticals.New.tclORELSE + (match is_unit_or_eq with + | Some _ -> + let hd,args = decompose_app t in + let (ind,_ as indu) = destInd hd in + let nparams = Inductiveops.inductive_nparams_env env ind in + let params = Util.List.firstn nparams args in + let p = applist ((mkConstructUi (indu,1)), params) in + (* Checking on the fly that it type-checks *) + simplest_elim (mkApp (mkVar id,[|p|])) + | None -> + Tacticals.New.tclZEROMSG (Pp.str"Not a negated unit type.")) (Proofview.tclORELSE (Proofview.Goal.enter { enter = begin fun gl -> let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in diff --git a/theories/Numbers/Integer/BigZ/ZMake.v b/theories/Numbers/Integer/BigZ/ZMake.v index 63fb5800c..fec6e0683 100644 --- a/theories/Numbers/Integer/BigZ/ZMake.v +++ b/theories/Numbers/Integer/BigZ/ZMake.v @@ -147,7 +147,7 @@ Module Make (NN:NType) <: ZType. Proof. apply Bool.eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min n m := match compare n m with Gt => m | _ => n end. diff --git a/theories/Numbers/Natural/BigN/NMake.v b/theories/Numbers/Natural/BigN/NMake.v index 98949736c..1425041a1 100644 --- a/theories/Numbers/Natural/BigN/NMake.v +++ b/theories/Numbers/Natural/BigN/NMake.v @@ -338,7 +338,7 @@ Module Make (W0:CyclicType) <: NType. Proof. apply eq_iff_eq_true. rewrite Z.leb_le. unfold Z.le, leb. rewrite spec_compare. - destruct Z.compare; split; try easy. now destruct 1. + now destruct Z.compare; split. Qed. Definition min (n m : t) : t := match compare n m with Gt => m | _ => n end. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index 954d3df20..b059173cb 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -448,7 +448,7 @@ Lemma leb_compare x y : (x <=? y) = match compare x y with Gt => false | _ => true end. Proof. apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff. -destruct compare; split; try easy. now destruct 1. +now destruct compare; split. Qed. End BoolOrderFacts. -- cgit v1.2.3 From 753248c145cdac846528d809a1f085c18408e17f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 15 Sep 2016 19:30:45 +0200 Subject: Added a test file for contradiction. --- test-suite/success/contradiction.v | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) create mode 100644 test-suite/success/contradiction.v diff --git a/test-suite/success/contradiction.v b/test-suite/success/contradiction.v new file mode 100644 index 000000000..92a7c6ccb --- /dev/null +++ b/test-suite/success/contradiction.v @@ -0,0 +1,32 @@ +(* Some tests for contradiction *) + +Lemma L1 : forall A B : Prop, A -> ~A -> B. +Proof. +intros; contradiction. +Qed. + +Lemma L2 : forall A B : Prop, ~A -> A -> B. +Proof. +intros; contradiction. +Qed. + +Lemma L3 : forall A : Prop, ~True -> A. +Proof. +intros; contradiction. +Qed. + +Lemma L4 : forall A : Prop, forall x : nat, ~x=x -> A. +Proof. +intros; contradiction. +Qed. + +Lemma L5 : forall A : Prop, forall x y : nat, ~x=y -> x=y -> A. +Proof. +intros; contradiction. +Qed. + +Lemma L6 : forall A : Prop, forall x y : nat, x=y -> ~x=y -> A. +Proof. +intros; contradiction. +Qed. + -- cgit v1.2.3 From 1a1af4f2119715245b8d4488664a8b57f4bdce08 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 4 Sep 2016 08:33:51 +0200 Subject: Adding variants enter_one and refine_one which assume that exactly one goal is under focus and which support returning a relevant output. --- engine/proofview.ml | 20 ++++++++++++++++++++ engine/proofview.mli | 4 ++++ proofs/refine.ml | 21 +++++++++++++++------ proofs/refine.mli | 3 +++ 4 files changed, 42 insertions(+), 6 deletions(-) diff --git a/engine/proofview.ml b/engine/proofview.ml index 576569cf5..a2838a2de 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1058,6 +1058,26 @@ module Goal = struct end end + exception NotExactlyOneSubgoal + let _ = CErrors.register_handler begin function + | NotExactlyOneSubgoal -> + CErrors.errorlabstrm "" (Pp.str"Not exactly one subgoal.") + | _ -> raise CErrors.Unhandled + end + + let enter_one f = + let open Proof in + Comb.get >>= function + | [goal] -> begin + Env.get >>= fun env -> + tclEVARMAP >>= fun sigma -> + try f.enter (gmake env sigma goal) + with e when catchable_exception e -> + let (e, info) = CErrors.push e in + tclZERO ~info e + end + | _ -> tclZERO NotExactlyOneSubgoal + type ('a, 'b) s_enter = { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } diff --git a/engine/proofview.mli b/engine/proofview.mli index 901cf26e0..bc68f11ff 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -499,6 +499,10 @@ module Goal : sig (** Like {!nf_enter}, but does not normalize the goal beforehand. *) val enter : ([ `LZ ], unit tactic) enter -> unit tactic + (** Like {!enter}, but assumes exactly one goal under focus, raising *) + (** an error otherwise. *) + val enter_one : ([ `LZ ], 'a tactic) enter -> 'a tactic + type ('a, 'b) s_enter = { s_enter : 'r. ('a, 'r) t -> ('b, 'r) Sigma.sigma } diff --git a/proofs/refine.ml b/proofs/refine.ml index af9be7897..dc6f4cea1 100644 --- a/proofs/refine.ml +++ b/proofs/refine.ml @@ -51,7 +51,8 @@ let typecheck_proof c concl env sigma = let (pr_constrv,pr_constr) = Hook.make ~default:(fun _env _sigma _c -> Pp.str"") () -let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl -> +let make_refine_enter ?(unsafe = true) f = + { enter = fun gl -> let gl = Proofview.Goal.assume gl in let sigma = Proofview.Goal.sigma gl in let sigma = Sigma.to_evar_map sigma in @@ -62,7 +63,7 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl -> let prev_future_goals = Evd.future_goals sigma in let prev_principal_goal = Evd.principal_future_goal sigma in (** Create the refinement term *) - let (c, sigma) = Sigma.run (Evd.reset_future_goals sigma) f in + let ((v,c), sigma) = Sigma.run (Evd.reset_future_goals sigma) f in let evs = Evd.future_goals sigma in let evkmain = Evd.principal_future_goal sigma in (** Check that the introduced evars are well-typed *) @@ -92,10 +93,18 @@ let refine ?(unsafe = true) f = Proofview.Goal.enter { enter = begin fun gl -> let comb = CList.map_filter (Proofview.Unsafe.advance sigma) (CList.rev evs) in let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in - Proofview.Trace.name_tactic trace (Proofview.tclUNIT ()) >>= fun () -> - Proofview.Unsafe.tclEVARS sigma >>= fun () -> - Proofview.Unsafe.tclSETGOALS comb -end } + Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v -> + Proofview.Unsafe.tclEVARS sigma <*> + Proofview.Unsafe.tclSETGOALS comb <*> + Proofview.tclUNIT v + } + +let refine_one ?(unsafe = true) f = + Proofview.Goal.enter_one (make_refine_enter ~unsafe f) + +let refine ?(unsafe = true) f = + let f = { run = fun sigma -> let Sigma (c,sigma,p) = f.run sigma in Sigma (((),c),sigma,p) } in + Proofview.Goal.enter (make_refine_enter ~unsafe f) (** Useful definitions *) diff --git a/proofs/refine.mli b/proofs/refine.mli index a9798b704..3d140f036 100644 --- a/proofs/refine.mli +++ b/proofs/refine.mli @@ -30,6 +30,9 @@ val refine : ?unsafe:bool -> Constr.t Sigma.run -> unit tactic tactic failures. If [unsafe] is [false] (default is [true]) [t] is type-checked beforehand. *) +val refine_one : ?unsafe:bool -> ('a * Constr.t) Sigma.run -> 'a tactic +(** A generalization of [refine] which assumes exactly one goal under focus *) + (** {7 Helper functions} *) val with_type : Environ.env -> Evd.evar_map -> -- cgit v1.2.3 From e6eef565639fb3840dd235eb675ece6e4dbeb082 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Fri, 16 Sep 2016 15:46:31 +0200 Subject: Addressing OCaml compilation warnings. One of them revealed a true bug. --- interp/notation_ops.ml | 2 +- parsing/egramcoq.ml | 1 - plugins/ssrmatching/ssrmatching.ml4 | 2 +- printing/pptactic.ml | 4 ++-- tactics/hipattern.ml | 2 +- 5 files changed, 5 insertions(+), 6 deletions(-) diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 1262864c7..1f29a2948 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -125,7 +125,7 @@ let rec cases_pattern_fold_map loc g e = function e', PatCstr (loc,cstr,patl',na') let subst_binder_type_vars l = function - | Evar_kinds.BinderType (Name id) as e -> + | Evar_kinds.BinderType (Name id) -> let id = try match Id.List.assoc id l with GVar(_,id') -> id' | _ -> id with Not_found -> id in diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 65d49cb45..a292c7463 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -449,7 +449,6 @@ let extend_constr state forpat ng = let isforpat = target_to_bool forpat in let needed_levels, state = register_empty_levels state isforpat pure_sublevels in let (pos,p4assoc,name,reinit), state = find_position state isforpat assoc level in - let nb_decls = List.length needed_levels + 1 in let empty_rules = List.map (prepare_empty_levels isforpat) needed_levels in let empty = { constrs = []; constrlists = []; binders = [] } in let act = ty_eval r (make_act forpat ng.notgram_notation) empty in diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4 index ff1db8cf5..a34fa4cae 100644 --- a/plugins/ssrmatching/ssrmatching.ml4 +++ b/plugins/ssrmatching/ssrmatching.ml4 @@ -903,7 +903,7 @@ let pr_ssrpattern_roundp _ _ _ = pr_pattern_roundp let wit_rpatternty = add_genarg "rpatternty" pr_pattern let glob_ssrterm gs = function - | k, (_, Some c) as x -> k, + | k, (_, Some c) -> k, let x = Tacintern.intern_constr gs c in fst x, Some c | ct -> ct diff --git a/printing/pptactic.ml b/printing/pptactic.ml index e2c78a507..f3117db17 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -802,7 +802,7 @@ module Make let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in - let pr_constrarg c = spc () ++ pr.pr_constr c in + let _pr_constrarg c = spc () ++ pr.pr_constr c in let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in let pr_intarg n = spc () ++ int n in @@ -850,7 +850,7 @@ module Make prlist pr_binder_fix bll ++ annot ++ str" :" ++ pr_lconstrarg ty ++ str")") in (* spc() ++ - hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg + hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg c) *) let pr_cofix_tac (id,c) = diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml index 6e24cc469..7b52a9cee 100644 --- a/tactics/hipattern.ml +++ b/tactics/hipattern.ml @@ -509,7 +509,7 @@ let coq_eqdec ~sum ~rev = let eqn = mkGAppRef coq_eq_ref (List.map mkGPatVar ["X1"; "X2"; "X3"]) in let args = [eqn; mkGAppRef coq_not_ref [eqn]] in let args = if rev then List.rev args else args in - mkPattern (mkGAppRef sum [eqn; mkGAppRef coq_not_ref [eqn]]) + mkPattern (mkGAppRef sum args) ) (** { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } *) -- cgit v1.2.3 From f1a561d847e207433a0ec3e6333798dfa19e4a0c Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 17 Sep 2016 20:24:36 +0200 Subject: Further "decide equality" tests on demand of Jason. --- test-suite/success/eqdecide.v | 12 ++++++++++++ theories/Structures/OrdersFacts.v | 2 +- 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/test-suite/success/eqdecide.v b/test-suite/success/eqdecide.v index 1f6af0dc4..724e2998e 100644 --- a/test-suite/success/eqdecide.v +++ b/test-suite/success/eqdecide.v @@ -14,6 +14,18 @@ Lemma lem1 : forall x y : T, {x = y} + {x <> y}. decide equality. Qed. +Lemma lem1' : forall x y : T, x = y \/ x <> y. + decide equality. +Qed. + +Lemma lem1'' : forall x y : T, {x <> y} + {x = y}. + decide equality. +Qed. + +Lemma lem1''' : forall x y : T, x <> y \/ x = y. + decide equality. +Qed. + Lemma lem2 : forall x y : T, {x = y} + {x <> y}. intros x y. decide equality. diff --git a/theories/Structures/OrdersFacts.v b/theories/Structures/OrdersFacts.v index b059173cb..6f8fc1b32 100644 --- a/theories/Structures/OrdersFacts.v +++ b/theories/Structures/OrdersFacts.v @@ -448,7 +448,7 @@ Lemma leb_compare x y : (x <=? y) = match compare x y with Gt => false | _ => true end. Proof. apply eq_true_iff_eq. rewrite leb_le, <- compare_le_iff. -now destruct compare; split. +now destruct compare. Qed. End BoolOrderFacts. -- cgit v1.2.3 From 1fda29d0179d60c83ead5db6e3062511aba7d264 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Mon, 19 Sep 2016 17:53:43 +0200 Subject: Fix warning when using Variables at toplevel. --- toplevel/command.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/toplevel/command.ml b/toplevel/command.ml index 097865648..12c387dcf 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -140,21 +140,21 @@ let check_definition (ce, evd, _, imps) = check_evars_are_solved (Global.env ()) evd (Evd.empty,evd); ce -let warn_local_let_definition = - CWarnings.create ~name:"local-let-definition" ~category:"scope" - (fun id -> - pr_id id ++ strbrk " is declared as a local definition") +let warn_local_declaration = + CWarnings.create ~name:"local-declaration" ~category:"scope" + (fun (id,kind) -> + pr_id id ++ strbrk " is declared as a local " ++ str kind) -let get_locality id = function +let get_locality id ~kind = function | Discharge -> (** If a Let is defined outside a section, then we consider it as a local definition *) - warn_local_let_definition id; + warn_local_declaration (id,kind); true | Local -> true | Global -> false let declare_global_definition ident ce local k pl imps = - let local = get_locality ident local in + let local = get_locality ident ~kind:"definition" local in let kn = declare_constant ident ~local (DefinitionEntry ce, IsDefinition k) in let gr = ConstRef kn in let () = maybe_declare_manual_implicits false gr imps in @@ -238,7 +238,7 @@ match local with (r,Univ.Instance.empty,true) | Global | Local | Discharge -> - let local = get_locality ident local in + let local = get_locality ident ~kind:"axiom" local in let inl = match nl with | NoInline -> None | DefaultInline -> Some (Flags.get_inline_level()) -- cgit v1.2.3 From c46981cfcdfe804178e1fe48a8489de6f7733c9c Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Sun, 18 Sep 2016 17:02:10 +0200 Subject: Fix typos in RefMan-uti.tex. - Ensure "coq_makefile --help" is properly typeset with HeVeA/PdfLaTeX - Replace 's with "s so they are typeset as true ASCII characters - Add missing ; before closing brace. --- doc/refman/RefMan-uti.tex | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index c282083b5..3bac7f5c1 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -102,7 +102,7 @@ generator using for instance the command: This command generates a file \texttt{Makefile} that can be used to compile all the sources of the current project. It follows the -syntax described by the output of \texttt{\% coq\_makefile ----help}. +syntax described by the output of \texttt{\% coq\_makefile -{}-help}. Once the \texttt{Makefile} file has been generated a first time, it can be used by the \texttt{make} command to compile part or all of the project. Note that once it has been generated once, as soon as @@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}. The following command generates a minimal example of \texttt{\_CoqProject} file: \begin{quotation} -\texttt{\% \{ echo '-R .} \textit{MyFancyLib} \texttt{' ; find . -name - '*.v' -print \} > \_CoqProject} +\texttt{\% \{ echo "-R .} \textit{MyFancyLib}\texttt{" ; find . -name + "*.v" -print ; \} > \_CoqProject} \end{quotation} when executed at the root of the directory containing the project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files -- cgit v1.2.3 From da708e759a1518bf4304e3d0edd725ed4176941f Mon Sep 17 00:00:00 2001 From: Erik Martin-Dorel Date: Mon, 19 Sep 2016 19:08:23 +0200 Subject: Replace { command ; } with ( command ) as suggested by Hugo. Also, escape the spaces after the dots to obtain a better PdfLaTeX output. --- doc/refman/RefMan-uti.tex | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/doc/refman/RefMan-uti.tex b/doc/refman/RefMan-uti.tex index 3bac7f5c1..f7d07772f 100644 --- a/doc/refman/RefMan-uti.tex +++ b/doc/refman/RefMan-uti.tex @@ -112,8 +112,8 @@ automatically regenerated by an invocation of \texttt{make}. The following command generates a minimal example of \texttt{\_CoqProject} file: \begin{quotation} -\texttt{\% \{ echo "-R .} \textit{MyFancyLib}\texttt{" ; find . -name - "*.v" -print ; \} > \_CoqProject} +\texttt{\% ( echo "-R .\ }\textit{MyFancyLib}\texttt{" ; find .\ -name + "*.v" -print ) > \_CoqProject} \end{quotation} when executed at the root of the directory containing the project. Here the \texttt{\_CoqProject} lists all the \texttt{.v} files -- cgit v1.2.3 From 97abe11a5ea271dcde5bd0aedd69056be22220eb Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Tue, 20 Sep 2016 09:09:23 +0200 Subject: Remove dead code in library/lib.ml. --- library/lib.ml | 30 ------------------------------ library/lib.mli | 9 --------- 2 files changed, 39 deletions(-) diff --git a/library/lib.ml b/library/lib.ml index 8880a8b15..7218950da 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -506,13 +506,6 @@ let section_instance = function let is_in_section ref = try ignore (section_instance ref); true with Not_found -> false -let full_replacement_context () = List.map pi2 !sectab -let full_section_segment_of_constant con = - List.map (fun (vars,_,(x,_)) -> fun hyps -> - named_of_variable_context - (try pi1 (Names.Cmap.find con x) - with Not_found -> fst (extract_hyps (vars, hyps)))) !sectab - (*************) (* Sections. *) @@ -613,15 +606,6 @@ let rec dp_of_mp = function |Names.MPbound _ -> library_dp () |Names.MPdot (mp,_) -> dp_of_mp mp -let rec split_mp = function - |Names.MPfile dp -> dp, Names.DirPath.empty - |Names.MPdot (prfx, lbl) -> - let mprec, dprec = split_mp prfx in - mprec, Libnames.add_dirpath_suffix dprec (Names.Label.to_id lbl) - |Names.MPbound mbid -> - let (_,id,dp) = Names.MBId.repr mbid in - library_dp (), Names.DirPath.make [id] - let rec split_modpath = function |Names.MPfile dp -> dp, [] |Names.MPbound mbid -> library_dp (), [Names.MBId.to_id mbid] @@ -633,20 +617,6 @@ let library_part = function |VarRef id -> library_dp () |ref -> dp_of_mp (mp_of_global ref) -let remove_section_part ref = - let sp = Nametab.path_of_global ref in - let dir,_ = repr_path sp in - match ref with - | VarRef id -> - anomaly (Pp.str "remove_section_part not supported on local variables") - | _ -> - if is_dirpath_prefix_of dir (cwd ()) then - (* Not yet (fully) discharged *) - pop_dirpath_n (sections_depth ()) (cwd ()) - else - (* Theorem/Lemma outside its outer section of definition *) - dir - (************************) (* Discharging names *) diff --git a/library/lib.mli b/library/lib.mli index 7080b5dba..0a70152ef 100644 --- a/library/lib.mli +++ b/library/lib.mli @@ -138,10 +138,8 @@ val library_dp : unit -> Names.DirPath.t (** Extract the library part of a name even if in a section *) val dp_of_mp : Names.module_path -> Names.DirPath.t -val split_mp : Names.module_path -> Names.DirPath.t * Names.DirPath.t val split_modpath : Names.module_path -> Names.DirPath.t * Names.Id.t list val library_part : Globnames.global_reference -> Names.DirPath.t -val remove_section_part : Globnames.global_reference -> Names.DirPath.t (** {6 Sections } *) @@ -191,10 +189,3 @@ val discharge_kn : Names.mutual_inductive -> Names.mutual_inductive val discharge_con : Names.constant -> Names.constant val discharge_global : Globnames.global_reference -> Globnames.global_reference val discharge_inductive : Names.inductive -> Names.inductive - -(* discharging a constant in one go *) -val full_replacement_context : unit -> Opaqueproof.work_list list -val full_section_segment_of_constant : - Names.constant -> (Context.Named.t -> Context.Named.t) list - - -- cgit v1.2.3 From 530287b4cd26b10457cad95dd6b41592e21ef440 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Wed, 21 Sep 2016 10:48:20 +0200 Subject: Fix description of change in intro semantics. --- CHANGES | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/CHANGES b/CHANGES index f7e1dee4c..c3eaae6ee 100644 --- a/CHANGES +++ b/CHANGES @@ -50,9 +50,10 @@ Tactics - Every generic argument type declares a tactic scope of the form "name:(...)" where name is the name of the argument. This generalizes the constr: and ltac: instances. -- When in strict mode (i.e. in a Ltac definition) the "intro" tactic cannot use - a locally free identifier anymore. It must use e.g. the "fresh" primitive - instead (potential source of incompatibilities). +- When in strict mode (i.e. in a Ltac definition), if the "intro" tactic is + given a free identifier, it is not bound in subsequent tactics anymore. + In order to introduce a binding, use e.g. the "fresh" primitive instead + (potential source of incompatibilities). - New tactics is_ind, is_const, is_proj, is_constructor for use in Ltac (DOC TODO). - New goal selectors. Sets of goals can be selected by select by listing integers ranges. Example: "1,4-7,24: tac" focuses "tac" on goals 1,4,5,6,7,24. -- cgit v1.2.3 From 464c680b631e1ba892f2171a36002d6ca184bc4f Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 22 Sep 2016 11:14:37 +0200 Subject: Fixing #5095 (non relevant too strict test in let-in abstraction). --- pretyping/unification.ml | 9 +-------- test-suite/bugs/closed/5095.v | 5 +++++ 2 files changed, 6 insertions(+), 8 deletions(-) create mode 100644 test-suite/bugs/closed/5095.v diff --git a/pretyping/unification.ml b/pretyping/unification.ml index cd0bbfa30..347bf6f9e 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1570,14 +1570,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl = let compute_dependency _ (hyp,_,_ as d) (sign,depdecls) = match occurrences_of_hyp hyp occs with | NoOccurrences, InHyp -> - if indirectly_dependent c d depdecls then - (* Told explicitly not to abstract over [d], but it is dependent *) - let id' = indirect_dependency d depdecls in - errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id' - ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp - ++ str ".") - else - (push_named_context_val d sign,depdecls) + (push_named_context_val d sign,depdecls) | AllOccurrences, InHyp as occ -> let occ = if likefirst then LikeFirst else AtOccs occ in let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in diff --git a/test-suite/bugs/closed/5095.v b/test-suite/bugs/closed/5095.v new file mode 100644 index 000000000..b6f38e3e8 --- /dev/null +++ b/test-suite/bugs/closed/5095.v @@ -0,0 +1,5 @@ +(* Checking let-in abstraction *) +Goal let x := Set in let y := x in True. + intros x y. + (* There used to have a too strict dependency test there *) + set (s := Set) in (value of x). -- cgit v1.2.3 From 505ac480574d235cd2f40ca4b2debde0bb875146 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 15 Sep 2016 17:32:22 +0200 Subject: typos --- interp/constrintern.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 30016dedc..4502aa7ac 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -33,10 +33,10 @@ open Context.Rel.Declaration (** constr_expr -> glob_constr translation: - it adds holes for implicit arguments - - it remplaces notations by their value (scopes stuff are here) + - it replaces notations by their value (scopes stuff are here) - it recognizes global vars from local ones - - it prepares pattern maching problems (a pattern becomes a tree where nodes - are constructor/variable pairs and leafs are variables) + - it prepares pattern matching problems (a pattern becomes a tree + where nodes are constructor/variable pairs and leafs are variables) All that at once, fasten your seatbelt! *) -- cgit v1.2.3 From 20d6c289bff303ec1a4cab3a56431989d0e527d2 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Thu, 22 Sep 2016 21:59:38 +0200 Subject: coqc -o now places .glob file near .vo file All compilation (by)products are placed where -o specifies. Used to be the case for .vo, .vio, .aux but not .glob --- interp/dumpglob.ml | 4 ++-- interp/dumpglob.mli | 2 +- toplevel/vernac.ml | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/interp/dumpglob.ml b/interp/dumpglob.ml index 1e14eeb81..b020f8945 100644 --- a/interp/dumpglob.ml +++ b/interp/dumpglob.ml @@ -45,10 +45,10 @@ let dump_string s = if dump () && !glob_output != Feedback then Pervasives.output_string !glob_file s -let start_dump_glob vfile = +let start_dump_glob ~vfile ~vofile = match !glob_output with | MultFiles -> - open_glob_file (Filename.chop_extension vfile ^ ".glob"); + open_glob_file (Filename.chop_extension vofile ^ ".glob"); output_string !glob_file "DIGEST "; output_string !glob_file (Digest.to_hex (Digest.file vfile)); output_char !glob_file '\n' diff --git a/interp/dumpglob.mli b/interp/dumpglob.mli index a7c799114..e84a64052 100644 --- a/interp/dumpglob.mli +++ b/interp/dumpglob.mli @@ -9,7 +9,7 @@ val open_glob_file : string -> unit val close_glob_file : unit -> unit -val start_dump_glob : string -> unit +val start_dump_glob : vfile:string -> vofile:string -> unit val end_dump_glob : unit -> unit val dump : unit -> bool diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index de3d14483..55f3a31a3 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -345,7 +345,7 @@ let compile verbosely f = Aux_file.(start_aux_file ~aux_file:(aux_file_name_for long_f_dot_vo) ~v_file:long_f_dot_v); - Dumpglob.start_dump_glob long_f_dot_v; + Dumpglob.start_dump_glob ~vfile:long_f_dot_v ~vofile:long_f_dot_vo; Dumpglob.dump_string ("F" ^ Names.DirPath.to_string ldir ^ "\n"); if !Flags.xml_export then Hook.get f_xml_start_library (); let wall_clock1 = Unix.gettimeofday () in -- cgit v1.2.3