From 82fe255fa41d22b07cee6ad65253707dbda7ce0b Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Thu, 6 Oct 2016 07:02:19 +0200 Subject: Fixing unexpected "noise" introduced in commit 24d5448c. A file was introduced by mistake in theories/Logic. --- theories/Logic/PropExtensionalityFacts.v | 88 -------------------------------- 1 file changed, 88 deletions(-) delete mode 100644 theories/Logic/PropExtensionalityFacts.v diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v deleted file mode 100644 index 6438fcd40d..0000000000 --- a/theories/Logic/PropExtensionalityFacts.v +++ /dev/null @@ -1,88 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* Proposition extensionality + Propositional functional extensionality - -2.2 Propositional extensionality -> Provable propositional extensionality -*) - -Set Implicit Arguments. - -(**********************************************************************) -(** * Definitions *) - -(** Propositional extensionality *) - -Local Notation PropositionalExtensionality := - (forall A B : Prop, (A <-> B) -> A = B). - -(** Provable-proposition extensionality *) - -Local Notation ProvablePropositionExtensionality := - (forall A:Prop, A -> A = True). - -(** Predicate extensionality *) - -Local Notation PredicateExtensionality := - (forall (A:Type) (P Q : A -> Prop), (forall x, P x <-> Q x) -> P = Q). - -(** Propositional functional extensionality *) - -Local Notation PropositionalFunctionalExtensionality := - (forall (A:Type) (P Q : A -> Prop), (forall x, P x = Q x) -> P = Q). - -(**********************************************************************) -(** * Propositional and predicate extensionality *) - -(**********************************************************************) -(** ** Predicate extensionality <-> Propositional extensionality + Propositional functional extensionality *) - -Lemma PredExt_imp_PropExt : PredicateExtensionality -> PropositionalExtensionality. -Proof. - intros Ext A B Equiv. - change A with ((fun _ => A) I). - now rewrite Ext with (P := fun _ : True =>A) (Q := fun _ => B). -Qed. - -Lemma PredExt_imp_PropFunExt : PredicateExtensionality -> PropositionalFunctionalExtensionality. -Proof. - intros Ext A P Q Eq. apply Ext. intros x. now rewrite (Eq x). -Qed. - -Lemma PropExt_and_PropFunExt_imp_PredExt : - PropositionalExtensionality -> PropositionalFunctionalExtensionality -> PredicateExtensionality. -Proof. - intros Ext FunExt A P Q Equiv. - apply FunExt. intros x. now apply Ext. -Qed. - -Theorem PropExt_and_PropFunExt_iff_PredExt : - PropositionalExtensionality /\ PropositionalFunctionalExtensionality <-> PredicateExtensionality. -Proof. - firstorder using PredExt_imp_PropExt, PredExt_imp_PropFunExt, PropExt_and_PropFunExt_imp_PredExt. -Qed. - -(**********************************************************************) -(** ** Propositional extensionality + Provable proposition extensionality *) - -Lemma PropExt_imp_ProvPropExt : PropositionalExtensionality -> ProvablePropositionExtensionality. -Proof. - intros Ext A Ha; apply Ext; split; trivial. -Qed. -- cgit v1.2.3 From 0b417c12eb10bb29bcee04384b6c0855cb9de73a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Wed, 5 Oct 2016 17:50:45 +0200 Subject: unification.ml: fix for bug #4763, unif regression Do not force all remaining conversions problems to be solved after the _first_ solution of an evar, but only at the end of assignment of terms to evars in w_merge. This was hell to track down, thanks for the help of Maxime. contribs pass and HoTT too. --- pretyping/evarsolve.ml | 2 ++ pretyping/unification.ml | 3 +-- test-suite/bugs/closed/4763.v | 13 +++++++++++++ 3 files changed, 16 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/4763.v diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 0db309f948..4084ee579a 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1580,6 +1580,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs = * ass. *) +(* This criterion relies on the fact that we postpone only problems of the form: +?x [?x1 ... ?xn] = t or the symmetric case. *) let status_changed lev (pbty,_,t1,t2) = (try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) || (try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 347bf6f9e5..3d734ea9a9 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1244,8 +1244,7 @@ let solve_simple_evar_eqn ts env evd ev rhs = match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with | UnifFailure (evd,reason) -> error_cannot_unify env evd ~reason (mkEvar ev,rhs); - | Success evd -> - Evarconv.consider_remaining_unif_problems env evd + | Success evd -> evd (* [w_merge env sigma b metas evars] merges common instances in metas or in evars, possibly generating new unification problems; if [b] diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v new file mode 100644 index 0000000000..ae8ed0e6e8 --- /dev/null +++ b/test-suite/bugs/closed/4763.v @@ -0,0 +1,13 @@ +Require Import Coq.Arith.Arith Coq.Classes.Morphisms Coq.Classes.RelationClasses. +Coercion is_true : bool >-> Sortclass. +Global Instance: Transitive leb. +Admitted. + +Goal forall x y z, leb x y -> leb y z -> True. + intros ??? H H'. + lazymatch goal with + | [ H : is_true (?R ?x ?y), H' : is_true (?R ?y ?z) |- _ ] + => pose proof (transitivity H H' : is_true (R x z)) + end. + exact I. +Qed. \ No newline at end of file -- cgit v1.2.3 From d0dda9c419894460de952d4b9342ea6518d24f83 Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 6 Oct 2016 11:14:08 +0200 Subject: Remove the Set Verbose Compat option and turn the warning on by default. These warnings can now be configured like any other, so we don't need a specific option anymore. --- CHANGES | 3 +++ interp/syntax_def.ml | 16 +--------------- interp/syntax_def.mli | 3 --- toplevel/coqtop.ml | 5 ----- 4 files changed, 4 insertions(+), 23 deletions(-) diff --git a/CHANGES b/CHANGES index a9ce5260a7..6ea680153d 100644 --- a/CHANGES +++ b/CHANGES @@ -100,6 +100,9 @@ Tools - Setting [Printing Dependent Evars Line] can be unset to disable the computation associated with printing the "dependent evars: " line in -emacs mode +- Removed the -verbose-compat-notations flag and the corresponding Set + Verbose Compat vernacular, since these warnings can now be silenced or + turned into errors using "-w". Changes from V8.5pl2 to V8.5pl3 =============================== diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index d2dcbd92aa..b2b82cce37 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -84,11 +84,6 @@ let declare_syntactic_definition local id onlyparse pat = let pr_syndef kn = pr_qualid (shortest_qualid_of_syndef Id.Set.empty kn) -let verbose_compat_notations = ref true - -let is_verbose_compat () = - !verbose_compat_notations - let pr_compat_warning (kn, def, v) = let pp_def = match def with | [], NRef r -> spc () ++ str "is" ++ spc () ++ pr_global_env Id.Set.empty r @@ -102,7 +97,7 @@ let warn_compatibility_notation = ~category:"deprecated" pr_compat_warning let verbose_compat kn def = function - | Some v when is_verbose_compat () && Flags.version_strictly_greater v -> + | Some v when Flags.version_strictly_greater v -> warn_compatibility_notation (kn, def, v) | _ -> () @@ -113,12 +108,3 @@ let search_syntactic_definition kn = def open Goptions - -let set_verbose_compat_notations = - declare_bool_option - { optsync = true; - optdepr = false; - optname = "verbose compatibility notations"; - optkey = ["Verbose";"Compat";"Notations"]; - optread = (fun () -> !verbose_compat_notations); - optwrite = ((:=) verbose_compat_notations) } diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli index aa2c9c3c1b..55e2848e69 100644 --- a/interp/syntax_def.mli +++ b/interp/syntax_def.mli @@ -17,6 +17,3 @@ val declare_syntactic_definition : bool -> Id.t -> Flags.compat_version option -> syndef_interpretation -> unit val search_syntactic_definition : kernel_name -> syndef_interpretation - -(** Option concerning verbose display of compatibility notations *) -val set_verbose_compat_notations : bool -> unit diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index 47d433d790..cf0efca69d 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -332,7 +332,6 @@ let error_missing_arg s = let filter_opts = ref false let exitcode () = if !filter_opts then 2 else 0 -let verb_compat_ntn = ref false let no_compat_ntn = ref false let print_where = ref false @@ -576,7 +575,6 @@ let parse_args arglist = |"-unicode" -> add_require "Utf8_core" |"-v"|"--version" -> Usage.version (exitcode ()) |"--print-version" -> Usage.machine_readable_version (exitcode ()) - |"-verbose-compat-notations" -> verb_compat_ntn := true |"-where" -> print_where := true |"-xml" -> Flags.xml_export := true @@ -637,9 +635,6 @@ let init_toplevel arglist = inputstate (); Mltop.init_known_plugins (); engage (); - (* Be careful to set these variables after the inputstate *) - Syntax_def.set_verbose_compat_notations !verb_compat_ntn; -(* Syntax_def.set_compat_notations (not !no_compat_ntn); FIXME *) if (not !batch_mode || List.is_empty !compile_list) && Global.env_is_initial () then Option.iter Declaremods.start_library !toplevel_name; -- cgit v1.2.3 From 5892f94fd5ca3a269e51eec26c3ff8f616ce02bd Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 6 Oct 2016 11:19:35 +0200 Subject: Remove the -no-compat-notations flag. This option was not doing anything... Today, one can turn the compatibility notations warning into an error, if ever that was the intended semantics. --- toplevel/coqtop.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml index cf0efca69d..ebdf804ba0 100644 --- a/toplevel/coqtop.ml +++ b/toplevel/coqtop.ml @@ -332,8 +332,6 @@ let error_missing_arg s = let filter_opts = ref false let exitcode () = if !filter_opts then 2 else 0 -let no_compat_ntn = ref false - let print_where = ref false let print_config = ref false let print_tags = ref false @@ -557,7 +555,6 @@ let parse_args arglist = |"-just-parsing" -> Vernac.just_parsing := true |"-m"|"--memory" -> memory_stat := true |"-noinit"|"-nois" -> load_init := false - |"-no-compat-notations" -> no_compat_ntn := true |"-no-glob"|"-noglob" -> Dumpglob.noglob (); glob_opt := true |"-native-compiler" -> if Coq_config.no_native_compiler then -- cgit v1.2.3 From 08f4cfc9dfb03973ae652ef6576342ae38f8f199 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 6 Oct 2016 11:21:10 +0200 Subject: w_merge: Add a comment about the (List.rev evars) This change exposed bug #4763 --- pretyping/unification.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 3d734ea9a9..b7edd6fcd6 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -1361,7 +1361,9 @@ let w_merge env with_types flags (evd,metas,evars) = in w_merge_rec evd [] [] eqns in let res = (* merge constraints *) - w_merge_rec evd (order_metas metas) (List.rev evars) [] + w_merge_rec evd (order_metas metas) + (* Assign evars in the order of assignments during unification *) + (List.rev evars) [] in if with_types then check_types res else res -- cgit v1.2.3 From bcecccc6973ab15bf99223764268808b89281964 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 6 Oct 2016 11:17:24 +0200 Subject: Removing a slow access to a named environment. --- kernel/csymtable.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml index 6f1ace25a6..c27cb04870 100644 --- a/kernel/csymtable.ml +++ b/kernel/csymtable.ml @@ -191,7 +191,7 @@ and slot_for_fv env fv = | None -> let open Context.Named in let open Declaration in - env.env_named_context.env_named_ctx |> lookup id |> get_value |> fill_fv_cache nv id val_of_named idfun + env |> Pre_env.lookup_named id |> get_value |> fill_fv_cache nv id val_of_named idfun | Some (v, _) -> v end | FVrel i -> -- cgit v1.2.3 From 0a6f0c161756a1878dd81e438df86f08631d8399 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Thu, 6 Oct 2016 11:38:06 +0200 Subject: evarconv.ml: Fix bug #4529, primproj unfolding Evarconv was made precociously dependent on user-declared reduction behaviors. Only cbn should rely on that. --- pretyping/evarconv.ml | 7 +------ test-suite/bugs/closed/4529.v | 45 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 46 insertions(+), 6 deletions(-) create mode 100644 test-suite/bugs/closed/4529.v diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index aead1cb35f..0d261f7f87 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -39,12 +39,7 @@ let _ = Goptions.declare_bool_option { let unfold_projection env evd ts p c = let cst = Projection.constant p in if is_transparent_constant ts cst then - let c' = Some (mkProj (Projection.make cst true, c)) in - match ReductionBehaviour.get (Globnames.ConstRef cst) with - | None -> c' - | Some (recargs, nargs, flags) -> - if (List.mem `ReductionNeverUnfold flags) then None - else c' + Some (mkProj (Projection.make cst true, c)) else None let eval_flexible_term ts env evd c = diff --git a/test-suite/bugs/closed/4529.v b/test-suite/bugs/closed/4529.v new file mode 100644 index 0000000000..8b3c24fec6 --- /dev/null +++ b/test-suite/bugs/closed/4529.v @@ -0,0 +1,45 @@ +(* File reduced by coq-bug-finder from original input, then from 1334 lines to 1518 lines, then from 849 lines to 59 lines *) +(* coqc version 8.5 (January 2016) compiled on Jan 22 2016 18:20:47 with OCaml 4.02.3 + coqtop version r-schnelltop:/home/r/src/coq/coq,(HEAD detached at V8.5) (5e23fb90b39dfa014ae5c4fb46eb713cca09dbff) *) +Require Coq.Setoids.Setoid. +Import Coq.Setoids.Setoid. + +Class Equiv A := equiv: relation A. +Infix "≡" := equiv (at level 70, no associativity). +Notation "(≡)" := equiv (only parsing). + +(* If I remove this line, everything compiles. *) +Set Primitive Projections. + +Class Dist A := dist : nat -> relation A. +Notation "x ={ n }= y" := (dist n x y) + (at level 70, n at next level, format "x ={ n }= y"). + +Record CofeMixin A `{Equiv A, Dist A} := { + mixin_equiv_dist x y : x ≡ y <-> forall n, x ={n}= y; + mixin_dist_equivalence n : Equivalence (dist n); +}. + +Structure cofeT := CofeT { + cofe_car :> Type; + cofe_equiv : Equiv cofe_car; + cofe_dist : Dist cofe_car; + cofe_mixin : CofeMixin cofe_car +}. +Existing Instances cofe_equiv cofe_dist. +Arguments cofe_car : simpl never. + +Section cofe_mixin. + Context {A : cofeT}. + Implicit Types x y : A. + Lemma equiv_dist x y : x ≡ y <-> forall n, x ={n}= y. +Admitted. +End cofe_mixin. + Context {A : cofeT}. + Global Instance cofe_equivalence : Equivalence ((≡) : relation A). + Proof. + split. + * + intros x. +apply equiv_dist. + -- cgit v1.2.3 From d180279aa934dfbb3fd97e707675b55f464f14ef Mon Sep 17 00:00:00 2001 From: Maxime Dénès Date: Thu, 6 Oct 2016 14:02:52 +0200 Subject: Disable compatibility notations warnings. Enablnig them would give a system that tells the user to replace e.g.: le_n_Sn with Nat.le_succ_diag_r lt_S with Nat.lt_lt_succ_r (on other types like R and and positive, the same lemma is called lt_lt_succ) In many cases, the new names will be too painful for intensive users. --- interp/syntax_def.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml index b2b82cce37..2523063e64 100644 --- a/interp/syntax_def.ml +++ b/interp/syntax_def.ml @@ -93,8 +93,8 @@ let pr_compat_warning (kn, def, v) = pr_syndef kn ++ pp_def ++ since let warn_compatibility_notation = - CWarnings.create ~name:"compatibility-notation" - ~category:"deprecated" pr_compat_warning + CWarnings.(create ~name:"compatibility-notation" + ~category:"deprecated" ~default:Disabled pr_compat_warning) let verbose_compat kn def = function | Some v when Flags.version_strictly_greater v -> -- cgit v1.2.3 From f4de78b048f6567f1e1fdd553b4f7ada0e0707b8 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Thu, 6 Oct 2016 20:45:05 +0200 Subject: Do not add "Append" as a lexer keyword. This was introduced to implement the Append feature on options. As usual when messing with predefined keywords, this broke code in the wild. In order not to create a new keyword, we do the string analysis on the production branch of parsing. --- parsing/g_vernac.ml4 | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index 96eede2b96..bc02a46218 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -850,9 +850,15 @@ GEXTEND Gram (* For acting on parameter tables *) | "Set"; table = option_table; v = option_value -> - VernacSetOption (table,v) - | "Set"; table = option_table; "Append"; v = STRING -> - VernacSetAppendOption (table,v) + begin match v with + | StringValue s -> + let (last, prefix) = List.sep_last table in + if String.equal last "Append" && not (List.is_empty prefix) then + VernacSetAppendOption (prefix, s) + else + VernacSetOption (table, v) + | _ -> VernacSetOption (table, v) + end | "Set"; table = option_table -> VernacSetOption (table,BoolValue true) | IDENT "Unset"; table = option_table -> -- cgit v1.2.3 From a2615bc47ed022ed4466741af3d4a29d45d05950 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Oct 2016 16:51:17 +0200 Subject: Fix bug #5125: Bad error message when attempting to use where with Class. --- toplevel/vernacentries.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml index d639811c56..feec23b50b 100644 --- a/toplevel/vernacentries.ml +++ b/toplevel/vernacentries.ml @@ -575,18 +575,18 @@ let vernac_inductive poly lo finite indl = | [ (_ , _ , _ ,Variant, RecordDecl _),_ ] -> CErrors.error "The Variant keyword cannot be used to define a record type. Use Record instead." | [ ( id , bl , c , b, RecordDecl (oc,fs) ), [] ] -> - vernac_record (match b with Class true -> Class false | _ -> b) + vernac_record (match b with Class _ -> Class false | _ -> b) poly finite id bl c oc fs - | [ ( id , bl , c , Class true, Constructors [l]), _ ] -> + | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> let f = let (coe, ((loc, id), ce)) = l in let coe' = if coe then Some true else None in (((coe', AssumExpr ((loc, Name id), ce)), None), []) in vernac_record (Class true) poly finite id bl c None [f] - | [ ( id , bl , c , Class true, _), _ ] -> - CErrors.error "Definitional classes must have a single method" - | [ ( id , bl , c , Class false, Constructors _), _ ] -> + | [ ( _ , _, _, Class _, Constructors _), [] ] -> CErrors.error "Inductive classes not supported" + | [ ( id , bl , c , Class _, _), _ :: _ ] -> + CErrors.error "where clause not supported for classes" | [ ( _ , _ , _ , _, RecordDecl _ ) , _ ] -> CErrors.error "where clause not supported for (co)inductive records" | _ -> let unpack = function -- cgit v1.2.3 From d93e8a7e7c9ae08cfedaf4a3db00ae3f9240bfe5 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Fri, 7 Oct 2016 18:06:47 +0200 Subject: Fix bug #4464: "Anomaly: variable H' unbound. Please report.". We simply catch the RetypeError raised by the retyping function and translate it into a user error, so that it is captured by the tactic monad instead of reaching toplevel. --- pretyping/retyping.mli | 2 ++ tactics/tactics.ml | 6 +++++- test-suite/bugs/closed/4464.v | 4 ++++ 3 files changed, 11 insertions(+), 1 deletion(-) create mode 100644 test-suite/bugs/closed/4464.v diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli index e4cca2679c..8ca40f829f 100644 --- a/pretyping/retyping.mli +++ b/pretyping/retyping.mli @@ -46,3 +46,5 @@ val type_of_global_reference_knowing_conclusion : val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr + +val print_retype_error : retype_error -> Pp.std_ppcmds diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 0629935e10..893f33f1a8 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -48,7 +48,11 @@ let inj_with_occurrences e = (AllOccurrences,e) let dloc = Loc.ghost -let typ_of env sigma c = Retyping.get_type_of env (Sigma.to_evar_map sigma) c +let typ_of env sigma c = + let open Retyping in + try get_type_of ~lax:true env (Sigma.to_evar_map sigma) c + with RetypeError e -> + user_err_loc (Loc.ghost, "", print_retype_error e) open Goptions diff --git a/test-suite/bugs/closed/4464.v b/test-suite/bugs/closed/4464.v new file mode 100644 index 0000000000..f8e9405d93 --- /dev/null +++ b/test-suite/bugs/closed/4464.v @@ -0,0 +1,4 @@ +Goal True -> True. +Proof. + intro H'. + let H := H' in destruct H; try destruct H. -- cgit v1.2.3 From 9bdd8aff92829aaa7c5a45b6e4e5adfa9e8789df Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 8 Oct 2016 00:10:55 +0200 Subject: Fix bug #5098: Symmetry broken in HoTT. We defactorize the in_clause grammar entry to allow parsing of the "symmetry" tactic when it has no arguments. Beforehand, the clause_dft_concl entry accepted the empty stream, preventing the definition of symmetry as a mere identifier. --- ltac/coretactics.ml4 | 5 ++++- ltac/extraargs.ml4 | 14 ++++++++++++++ ltac/extraargs.mli | 5 +++++ parsing/g_tactic.ml4 | 2 +- parsing/pcoq.ml | 1 + parsing/pcoq.mli | 1 + printing/pptactic.ml | 19 +++++++++++++++---- printing/pptacticsig.mli | 3 +++ 8 files changed, 44 insertions(+), 6 deletions(-) diff --git a/ltac/coretactics.ml4 b/ltac/coretactics.ml4 index de4d589eee..6186667584 100644 --- a/ltac/coretactics.ml4 +++ b/ltac/coretactics.ml4 @@ -151,7 +151,10 @@ END TACTIC EXTEND symmetry [ "symmetry" ] -> [ Tactics.intros_symmetry {onhyps=Some[];concl_occs=AllOccurrences} ] -| [ "symmetry" clause_dft_concl(cl) ] -> [ Tactics.intros_symmetry cl ] +END + +TACTIC EXTEND symmetry_in +| [ "symmetry" "in" in_clause(cl) ] -> [ Tactics.intros_symmetry cl ] END (** Split *) diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4 index c6d72e03e2..0db1cd7bae 100644 --- a/ltac/extraargs.ml4 +++ b/ltac/extraargs.ml4 @@ -260,6 +260,20 @@ END let pr_by_arg_tac prtac opt_c = pr_by_arg_tac () () prtac opt_c +let pr_in_clause _ _ _ cl = Pptactic.pr_in_clause Ppconstr.pr_lident cl +let pr_in_top_clause _ _ _ cl = Pptactic.pr_in_clause Id.print cl +let in_clause' = Pcoq.Tactic.in_clause + +ARGUMENT EXTEND in_clause + TYPED AS clause_dft_concl + PRINTED BY pr_in_top_clause + RAW_TYPED AS clause_dft_concl + RAW_PRINTED BY pr_in_clause + GLOB_TYPED AS clause_dft_concl + GLOB_PRINTED BY pr_in_clause +| [ in_clause'(cl) ] -> [ cl ] +END + (* spiwack: the print functions are incomplete, but I don't know what they are used for *) let pr_r_nat_field natf = diff --git a/ltac/extraargs.mli b/ltac/extraargs.mli index 0cf77935c2..b12187e18a 100644 --- a/ltac/extraargs.mli +++ b/ltac/extraargs.mli @@ -71,3 +71,8 @@ val pr_by_arg_tac : val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val wit_retroknowledge_field : (Retroknowledge.field, unit, unit) Genarg.genarg_type + +val wit_in_clause : + (Id.t Loc.located Locus.clause_expr, + Id.t Loc.located Locus.clause_expr, + Id.t Locus.clause_expr) Genarg.genarg_type diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 199ef9fcee..3152afb28d 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -220,7 +220,7 @@ let warn_deprecated_eqn_syntax = GEXTEND Gram GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis bindings red_expr int_or_var open_constr uconstr - simple_intropattern clause_dft_concl hypident destruction_arg; + simple_intropattern in_clause clause_dft_concl hypident destruction_arg; int_or_var: [ [ n = integer -> ArgArg n diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 4e069c9e33..9e9a7e723e 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -350,6 +350,7 @@ module Tactic = let red_expr = make_gen_entry utactic "red_expr" let simple_intropattern = make_gen_entry utactic "simple_intropattern" + let in_clause = make_gen_entry utactic "in_clause" let clause_dft_concl = make_gen_entry utactic "clause" diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 7f49c997fe..7f6caf63fb 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -193,6 +193,7 @@ module Tactic : val red_expr : raw_red_expr Gram.entry val simple_tactic : raw_tactic_expr Gram.entry val simple_intropattern : constr_expr intro_pattern_expr located Gram.entry + val in_clause : Names.Id.t Loc.located Locus.clause_expr Gram.entry val clause_dft_concl : Names.Id.t Loc.located Locus.clause_expr Gram.entry val tactic_arg : raw_tactic_arg Gram.entry val tactic_expr : raw_tactic_expr Gram.entry diff --git a/printing/pptactic.ml b/printing/pptactic.ml index f3117db170..1e618b59eb 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -583,13 +583,13 @@ module Make | None -> mt() let pr_hyp_location pr_id = function - | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs + | occs, InHyp -> pr_with_occurrences pr_id occs | occs, InHypTypeOnly -> - spc () ++ pr_with_occurrences (fun id -> + pr_with_occurrences (fun id -> str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")" ) occs | occs, InHypValueOnly -> - spc () ++ pr_with_occurrences (fun id -> + pr_with_occurrences (fun id -> str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")" ) occs @@ -603,6 +603,17 @@ module Make | None -> mt () | Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat + let pr_in_clause pr_id = function + | { onhyps=None; concl_occs=NoOccurrences } -> + (str "* |-") + | { onhyps=None; concl_occs=occs } -> + (pr_with_occurrences (fun () -> str "*") (occs,())) + | { onhyps=Some l; concl_occs=NoOccurrences } -> + prlist_with_sep (fun () -> str ", ") (pr_hyp_location pr_id) l + | { onhyps=Some l; concl_occs=occs } -> + let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in + (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) + let pr_clauses default_is_concl pr_id = function | { onhyps=Some []; concl_occs=occs } when (match default_is_concl with Some true -> true | _ -> false) -> @@ -619,7 +630,7 @@ module Make | _ -> pr_with_occurrences (fun () -> str" |- *") (occs,()) in pr_in - (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs) + (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs) let pr_orient b = if b then mt () else str "<- " diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli index c08d6044db..665e055f23 100644 --- a/printing/pptacticsig.mli +++ b/printing/pptacticsig.mli @@ -29,6 +29,9 @@ module type Pp = sig val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds + val pr_in_clause : + ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds + val pr_clauses : bool option -> ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds -- cgit v1.2.3 From 6e8787737a0eae9ed8aa5b1696a94495e7cb6020 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 8 Oct 2016 01:46:09 +0200 Subject: Fix bug #5066: Anomaly: cannot find Coq.Logic.JMeq.JMeq. --- pretyping/program.ml | 6 ++++-- test-suite/bugs/closed/5066.v | 7 +++++++ 2 files changed, 11 insertions(+), 2 deletions(-) create mode 100644 test-suite/bugs/closed/5066.v diff --git a/pretyping/program.ml b/pretyping/program.ml index b4333847b7..62aedcfbf6 100644 --- a/pretyping/program.ml +++ b/pretyping/program.ml @@ -15,10 +15,12 @@ open Term let make_dir l = DirPath.make (List.rev_map Id.of_string l) let find_reference locstr dir s = - let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in + let dp = make_dir dir in + let sp = Libnames.make_path dp (Id.of_string s) in try Nametab.global_of_path sp with Not_found -> - anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp) + user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++ + str " has to be required first.") let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s) diff --git a/test-suite/bugs/closed/5066.v b/test-suite/bugs/closed/5066.v new file mode 100644 index 0000000000..eed7f0f3ff --- /dev/null +++ b/test-suite/bugs/closed/5066.v @@ -0,0 +1,7 @@ +Require Import Vector. + +Fail Program Fixpoint vector_rev {A : Type} {n1 n2 : nat} (v1 : Vector.t A n1) (v2 : Vector.t A n2) : Vector.t A (n1+n2) := + match v1 with + | nil _ => v2 + | cons _ e n' sv => vector_rev sv (cons A e n2 v2) + end. -- cgit v1.2.3 From 5c07e11226e44dadb04a2fe48c91cce094989ce0 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 8 Oct 2016 12:00:56 +0200 Subject: Report about changes of semantics of auto as an ltac argument (see #4966). --- CHANGES | 3 +++ 1 file changed, 3 insertions(+) diff --git a/CHANGES b/CHANGES index 6ea680153d..0210281c3a 100644 --- a/CHANGES +++ b/CHANGES @@ -14,6 +14,9 @@ Bugfixes binders made more robust. - #4780: Induction with universe polymorphism on was creating ill-typed terms. - #3070: fixing "subst" in the presence of a chain of dependencies. +- When used as an argument of an ltac function, "auto" without "with" + nor "using" clause now correctly uses only the core hint database by + default. Specification language -- cgit v1.2.3 From 8110e9cbd6d70960a221c316774460f6ad6dc5e9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Tue, 13 Sep 2016 12:43:52 +0200 Subject: Adding debugging printer for Genarg.ArgT.t. --- dev/db | 1 + dev/top_printers.ml | 2 ++ 2 files changed, 3 insertions(+) diff --git a/dev/db b/dev/db index 86e35a3ece..f226291d64 100644 --- a/dev/db +++ b/dev/db @@ -51,6 +51,7 @@ install_printer Top_printers.prsubst install_printer Top_printers.prdelta install_printer Top_printers.ppfconstr install_printer Top_printers.ppgenarginfo +install_printer Top_printers.ppgenargargt install_printer Top_printers.ppist install_printer Top_printers.ppconstrunderbindersidmap install_printer Top_printers.ppunbound_ltac_var_map diff --git a/dev/top_printers.ml b/dev/top_printers.ml index e09477014b..e34385e5c3 100644 --- a/dev/top_printers.ml +++ b/dev/top_printers.ml @@ -478,6 +478,8 @@ let prgenarginfo arg = let ppgenarginfo arg = pp (prgenarginfo arg) +let ppgenargargt arg = pp (str (Genarg.ArgT.repr arg)) + let ppist ist = let pr id arg = prgenarginfo arg in pp (pridmap pr ist.Geninterp.lfun) -- cgit v1.2.3