aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES6
-rw-r--r--dev/db1
-rw-r--r--dev/top_printers.ml2
-rw-r--r--interp/syntax_def.ml20
-rw-r--r--interp/syntax_def.mli3
-rw-r--r--ltac/coretactics.ml45
-rw-r--r--ltac/extraargs.ml414
-rw-r--r--ltac/extraargs.mli5
-rw-r--r--ltac/g_tactic.ml42
-rw-r--r--ltac/pltac.ml1
-rw-r--r--ltac/pltac.mli1
-rw-r--r--ltac/pptactic.ml19
-rw-r--r--ltac/pptacticsig.mli3
-rw-r--r--parsing/g_vernac.ml412
-rw-r--r--pretyping/evarconv.ml7
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/program.ml6
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/unification.ml7
-rw-r--r--tactics/tactics.ml6
-rw-r--r--test-suite/bugs/closed/4464.v4
-rw-r--r--test-suite/bugs/closed/4529.v45
-rw-r--r--test-suite/bugs/closed/4763.v13
-rw-r--r--test-suite/bugs/closed/5066.v7
-rw-r--r--theories/Logic/PropExtensionalityFacts.v88
-rw-r--r--toplevel/coqtop.ml8
-rw-r--r--toplevel/vernacentries.ml10
27 files changed, 157 insertions, 142 deletions
diff --git a/CHANGES b/CHANGES
index a9ce5260a..0210281c3 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
@@ -100,6 +103,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/dev/db b/dev/db
index 1282352e6..d3503ef43 100644
--- a/dev/db
+++ b/dev/db
@@ -52,6 +52,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 f99132a67..71a420754 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)
diff --git a/interp/syntax_def.ml b/interp/syntax_def.ml
index 870b4bbcf..c3f4c4f30 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
@@ -98,11 +93,11 @@ 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 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 aa2c9c3c1..55e2848e6 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/ltac/coretactics.ml4 b/ltac/coretactics.ml4
index b6d731f9f..28ff6df83 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 8a316419e..53b726432 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' = Pltac.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 0cf77935c..b12187e18 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/ltac/g_tactic.ml4 b/ltac/g_tactic.ml4
index 4e657fe83..685c07c9a 100644
--- a/ltac/g_tactic.ml4
+++ b/ltac/g_tactic.ml4
@@ -222,7 +222,7 @@ open Vernac_
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/ltac/pltac.ml b/ltac/pltac.ml
index fb5204d89..1d21118ae 100644
--- a/ltac/pltac.ml
+++ b/ltac/pltac.ml
@@ -33,6 +33,7 @@ let destruction_arg = make_gen_entry utactic "destruction_arg"
let int_or_var = make_gen_entry utactic "int_or_var"
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/ltac/pltac.mli b/ltac/pltac.mli
index 27eb9f280..810e1ec39 100644
--- a/ltac/pltac.mli
+++ b/ltac/pltac.mli
@@ -29,6 +29,7 @@ val destruction_arg : constr_expr with_bindings destruction_arg Gram.entry
val int_or_var : int or_var 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/ltac/pptactic.ml b/ltac/pptactic.ml
index 80cafb3ab..6230fa060 100644
--- a/ltac/pptactic.ml
+++ b/ltac/pptactic.ml
@@ -450,13 +450,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
@@ -470,6 +470,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) ->
@@ -486,7 +497,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/ltac/pptacticsig.mli b/ltac/pptacticsig.mli
index 455cc1be1..74ddd377a 100644
--- a/ltac/pptacticsig.mli
+++ b/ltac/pptacticsig.mli
@@ -27,6 +27,9 @@ module type Pp = sig
val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> 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
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index ad6ad9340..cb521ec54 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 ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b7fc2de95..51d006e25 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -45,12 +45,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/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a744f5ec6..c44903e8c 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1591,6 +1591,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/program.ml b/pretyping/program.ml
index b4333847b..4b6137b53 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 (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/pretyping/retyping.mli b/pretyping/retyping.mli
index e4cca2679..8ca40f829 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/pretyping/unification.ml b/pretyping/unification.ml
index 5d6c41103..a96a496b8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1270,8 +1270,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]
@@ -1390,7 +1389,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
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 8e7f4613c..de328e23f 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -52,7 +52,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 (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 000000000..f8e9405d9
--- /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.
diff --git a/test-suite/bugs/closed/4529.v b/test-suite/bugs/closed/4529.v
new file mode 100644
index 000000000..8b3c24fec
--- /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.
+
diff --git a/test-suite/bugs/closed/4763.v b/test-suite/bugs/closed/4763.v
new file mode 100644
index 000000000..ae8ed0e6e
--- /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
diff --git a/test-suite/bugs/closed/5066.v b/test-suite/bugs/closed/5066.v
new file mode 100644
index 000000000..eed7f0f3f
--- /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.
diff --git a/theories/Logic/PropExtensionalityFacts.v b/theories/Logic/PropExtensionalityFacts.v
deleted file mode 100644
index 6438fcd40..000000000
--- a/theories/Logic/PropExtensionalityFacts.v
+++ /dev/null
@@ -1,88 +0,0 @@
-(************************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
-(* \VV/ **************************************************************)
-(* // * This file is distributed under the terms of the *)
-(* * GNU Lesser General Public License Version 2.1 *)
-(************************************************************************)
-
-(** Some facts and definitions about propositional and predicate extensionality
-
-We investigate the relations between the following extensionality principles
-
-- Provable-proposition extensionality
-- Predicate extensionality
-- Propositional functional extensionality
-
-Table of contents
-
-1. Definitions
-
-2.1 Predicate extensionality <-> 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.
diff --git a/toplevel/coqtop.ml b/toplevel/coqtop.ml
index 47d433d79..ebdf804ba 100644
--- a/toplevel/coqtop.ml
+++ b/toplevel/coqtop.ml
@@ -332,9 +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
let print_config = ref false
let print_tags = ref false
@@ -558,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
@@ -576,7 +572,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 +632,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;
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 9415ade28..607bb6cfb 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -576,18 +576,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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-01 08:15:36 +0000