aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rwxr-xr-xdev/make-installer-win32.sh2
-rwxr-xr-xdev/make-installer-win64.sh2
-rwxr-xr-xdev/nsis/coq.nsi2
-rw-r--r--ltac/rewrite.ml2
-rw-r--r--plugins/cc/ccalgo.ml28
-rw-r--r--plugins/cc/ccalgo.mli2
-rw-r--r--plugins/cc/ccproof.ml12
-rw-r--r--plugins/cc/cctac.ml8
-rw-r--r--tactics/tactics.ml6
-rw-r--r--test-suite/bugs/closed/2848.v7
-rw-r--r--test-suite/bugs/closed/4656.v4
-rw-r--r--test-suite/success/Compat84.v19
-rw-r--r--theories/Compat/Coq84.v27
-rw-r--r--toplevel/classes.ml4
-rw-r--r--toplevel/classes.mli1
15 files changed, 83 insertions, 43 deletions
diff --git a/dev/make-installer-win32.sh b/dev/make-installer-win32.sh
index d405e66cc..51d428dd1 100755
--- a/dev/make-installer-win32.sh
+++ b/dev/make-installer-win32.sh
@@ -16,7 +16,7 @@ if [ ! -e bin/make.exe ]; then
fi
VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win32" coq.nsi
echo Installer:
ls -h $PWD/*exe
cd ../..
diff --git a/dev/make-installer-win64.sh b/dev/make-installer-win64.sh
index 2f765c1a1..438f4ae5b 100755
--- a/dev/make-installer-win64.sh
+++ b/dev/make-installer-win64.sh
@@ -22,7 +22,7 @@ if [ ! -e bin/make.exe ]; then
fi
VERSION=`grep ^VERSION= config/Makefile | cut -d = -f 2`
cd dev/nsis
-"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" coq.nsi
+"$NSIS" -DVERSION=$VERSION -DGTK_RUNTIME="`cygpath -w $BASE`" -DARCH="win64" coq.nsi
echo Installer:
ls -h $PWD/*exe
cd ../..
diff --git a/dev/nsis/coq.nsi b/dev/nsis/coq.nsi
index 676490510..e1052b1e1 100755
--- a/dev/nsis/coq.nsi
+++ b/dev/nsis/coq.nsi
@@ -13,7 +13,7 @@ SetCompressor lzma
!define MY_PRODUCT "Coq" ;Define your own software name here
!define COQ_SRC_PATH "..\.."
-!define OUTFILE "coq-installer-${VERSION}.exe"
+!define OUTFILE "coq-installer-${VERSION}-${ARCH}.exe"
!include "MUI2.nsh"
!include "FileAssociation.nsh"
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index cf2a01052..97b2393a8 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1749,7 +1749,7 @@ let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
let anew_instance global binders instance fields =
new_instance (Flags.is_universe_polymorphism ())
binders instance (Some (true, CRecord (Loc.ghost,fields)))
- ~global ~generalize:false None
+ ~global ~generalize:false ~refine:false None
let declare_instance_refl global binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 359157a4c..c01214377 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -25,7 +25,7 @@ let init_size=5
let cc_verbose=ref false
let debug x =
- if !cc_verbose then msg_debug x
+ if !cc_verbose then msg_debug (x ())
let _=
let gdopt=
@@ -603,7 +603,7 @@ let add_inst state (inst,int_subst) =
Control.check_for_interrupt ();
if state.rew_depth > 0 then
if is_redundant state inst.qe_hyp_id int_subst then
- debug (str "discarding redundant (dis)equality")
+ debug (fun () -> str "discarding redundant (dis)equality")
else
begin
Identhash.add state.q_history inst.qe_hyp_id int_subst;
@@ -618,7 +618,7 @@ let add_inst state (inst,int_subst) =
state.rew_depth<-pred state.rew_depth;
if inst.qe_pol then
begin
- debug (
+ debug (fun () ->
(str "Adding new equality, depth="++ int state.rew_depth) ++ fnl () ++
(str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " == " ++ pr_term t ++ str "]"));
@@ -626,7 +626,7 @@ let add_inst state (inst,int_subst) =
end
else
begin
- debug (
+ debug (fun () ->
(str "Adding new disequality, depth="++ int state.rew_depth) ++ fnl () ++
(str " [" ++ Termops.print_constr prf ++ str " : " ++
pr_term s ++ str " <> " ++ pr_term t ++ str "]"));
@@ -657,7 +657,7 @@ let join_path uf i j=
min_path (down_path uf i [],down_path uf j [])
let union state i1 i2 eq=
- debug (str "Linking " ++ pr_idx_term state.uf i1 ++
+ debug (fun () -> str "Linking " ++ pr_idx_term state.uf i1 ++
str " and " ++ pr_idx_term state.uf i2 ++ str ".");
let r1= get_representative state.uf i1
and r2= get_representative state.uf i2 in
@@ -698,7 +698,7 @@ let union state i1 i2 eq=
let merge eq state = (* merge and no-merge *)
debug
- (str "Merging " ++ pr_idx_term state.uf eq.lhs ++
+ (fun () -> str "Merging " ++ pr_idx_term state.uf eq.lhs ++
str " and " ++ pr_idx_term state.uf eq.rhs ++ str ".");
let uf=state.uf in
let i=find uf eq.lhs
@@ -711,7 +711,7 @@ let merge eq state = (* merge and no-merge *)
let update t state = (* update 1 and 2 *)
debug
- (str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Updating term " ++ pr_idx_term state.uf t ++ str ".");
let (i,j) as sign = signature state.uf t in
let (u,v) = subterms state.uf t in
let rep = get_representative state.uf i in
@@ -773,7 +773,7 @@ let process_constructor_mark t i rep pac state =
let process_mark t m state =
debug
- (str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
+ (fun () -> str "Processing mark for term " ++ pr_idx_term state.uf t ++ str ".");
let i=find state.uf t in
let rep=get_representative state.uf i in
match m with
@@ -794,7 +794,7 @@ let check_disequalities state =
else (str "No", check_aux q)
in
let _ = debug
- (str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
+ (fun () -> str "Checking if " ++ pr_idx_term state.uf dis.lhs ++ str " = " ++
pr_idx_term state.uf dis.rhs ++ str " ... " ++ info) in
ans
| [] -> None
@@ -979,7 +979,7 @@ let find_instances state =
let pb_stack= init_pb_stack state in
let res =ref [] in
let _ =
- debug (str "Running E-matching algorithm ... ");
+ debug (fun () -> str "Running E-matching algorithm ... ");
try
while true do
Control.check_for_interrupt ();
@@ -990,7 +990,7 @@ let find_instances state =
!res
let rec execute first_run state =
- debug (str "Executing ... ");
+ debug (fun () -> str "Executing ... ");
try
while
Control.check_for_interrupt ();
@@ -1000,7 +1000,7 @@ let rec execute first_run state =
None ->
if not(Int.Set.is_empty state.pa_classes) then
begin
- debug (str "First run was incomplete, completing ... ");
+ debug (fun () -> str "First run was incomplete, completing ... ");
complete state;
execute false state
end
@@ -1015,12 +1015,12 @@ let rec execute first_run state =
end
else
begin
- debug (str "Out of instances ... ");
+ debug (fun () -> str "Out of instances ... ");
None
end
else
begin
- debug (str "Out of depth ... ");
+ debug (fun () -> str "Out of depth ... ");
None
end
| Some dis -> Some
diff --git a/plugins/cc/ccalgo.mli b/plugins/cc/ccalgo.mli
index b73c8eef8..c7fa2f56f 100644
--- a/plugins/cc/ccalgo.mli
+++ b/plugins/cc/ccalgo.mli
@@ -120,7 +120,7 @@ val term_equal : term -> term -> bool
val constr_of_term : term -> constr
-val debug : Pp.std_ppcmds -> unit
+val debug : (unit -> Pp.std_ppcmds) -> unit
val forest : state -> forest
diff --git a/plugins/cc/ccproof.ml b/plugins/cc/ccproof.ml
index c188bf3bc..d2bbaf6a7 100644
--- a/plugins/cc/ccproof.ml
+++ b/plugins/cc/ccproof.ml
@@ -93,13 +93,13 @@ let pinject p c n a =
p_rule=Inject(p,c,n,a)}
let rec equal_proof uf i j=
- debug (str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "equal_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
if i=j then prefl (term uf i) else
let (li,lj)=join_path uf i j in
ptrans (path_proof uf i li) (psym (path_proof uf j lj))
and edge_proof uf ((i,j),eq)=
- debug (str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "edge_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let pi=equal_proof uf i eq.lhs in
let pj=psym (equal_proof uf j eq.rhs) in
let pij=
@@ -115,7 +115,7 @@ and edge_proof uf ((i,j),eq)=
ptrans (ptrans pi pij) pj
and constr_proof uf i ipac=
- debug (str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
+ debug (fun () -> str "constr_proof " ++ pr_idx_term uf i ++ brk (1,20));
let t=find_oldest_pac uf i ipac in
let eq_it=equal_proof uf i t in
if ipac.args=[] then
@@ -128,20 +128,20 @@ and constr_proof uf i ipac=
ptrans eq_it (pcongr p (prefl targ))
and path_proof uf i l=
- debug (str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
+ debug (fun () -> str "path_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ str "{" ++
(prlist_with_sep (fun () -> str ",") (fun ((_,j),_) -> int j) l) ++ str "}");
match l with
| [] -> prefl (term uf i)
| x::q->ptrans (path_proof uf (snd (fst x)) q) (edge_proof uf x)
and congr_proof uf i j=
- debug (str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "congr_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let (i1,i2) = subterms uf i
and (j1,j2) = subterms uf j in
pcongr (equal_proof uf i1 j1) (equal_proof uf i2 j2)
and ind_proof uf i ipac j jpac=
- debug (str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
+ debug (fun () -> str "ind_proof " ++ pr_idx_term uf i ++ brk (1,20) ++ pr_idx_term uf j);
let p=equal_proof uf i j
and p1=constr_proof uf i ipac
and p2=constr_proof uf j jpac in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index a1aff12d4..c8924073c 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -401,16 +401,16 @@ let build_term_to_complete uf meta pac =
let cc_tactic depth additionnal_terms =
Proofview.Goal.nf_enter { enter = begin fun gl ->
Coqlib.check_required_library Coqlib.logic_module_name;
- let _ = debug (Pp.str "Reading subgoal ...") in
+ let _ = debug (fun () -> Pp.str "Reading subgoal ...") in
let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
- let _ = debug (Pp.str "Problem built, solving ...") in
+ let _ = debug (fun () -> Pp.str "Problem built, solving ...") in
let sol = execute true state in
- let _ = debug (Pp.str "Computation completed.") in
+ let _ = debug (fun () -> Pp.str "Computation completed.") in
let uf=forest state in
match sol with
None -> Tacticals.New.tclFAIL 0 (str "congruence failed")
| Some reason ->
- debug (Pp.str "Goal solved, generating proof ...");
+ debug (fun () -> Pp.str "Goal solved, generating proof ...");
match reason with
Discrimination (i,ipac,j,jpac) ->
let p=build_proof uf (`Discr (i,ipac,j,jpac)) in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 7ae178af5..a626092dd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1468,7 +1468,8 @@ let descend_in_conjunctions avoid tac (err, info) c =
let sigma = Sigma.Unsafe.of_evar_map sigma in
let Sigma (elim, _, _) = build_case_analysis_scheme env sigma (ind,u) false sort in
NotADefinedRecordUseScheme elim in
- Tacticals.New.tclFIRST
+ Tacticals.New.tclORELSE0
+ (Tacticals.New.tclFIRST
(List.init n (fun i ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
@@ -1481,7 +1482,8 @@ let descend_in_conjunctions avoid tac (err, info) c =
[Proofview.V82.tactic (refine p);
(* Might be ill-typed due to forbidden elimination. *)
Tacticals.New.onLastHypId (tac (not isrec))]
- end }))
+ end })))
+ (Proofview.tclZERO ~info err)
| None -> Proofview.tclZERO ~info err
with RefinerError _|UserError _ -> Proofview.tclZERO ~info err
end }
diff --git a/test-suite/bugs/closed/2848.v b/test-suite/bugs/closed/2848.v
index de137d39d..828e3b8c1 100644
--- a/test-suite/bugs/closed/2848.v
+++ b/test-suite/bugs/closed/2848.v
@@ -2,8 +2,9 @@ Require Import Setoid.
Parameter value' : Type.
Parameter equiv' : value' -> value' -> Prop.
-
+Axiom cheat : forall {A}, A.
Add Parametric Relation : _ equiv'
- reflexivity proved by (Equivalence.equiv_reflexive _)
- transitivity proved by (Equivalence.equiv_transitive _)
+ reflexivity proved by (Equivalence.equiv_reflexive cheat)
+ transitivity proved by (Equivalence.equiv_transitive cheat)
as apply_equiv'_rel.
+Check apply_equiv'_rel : PreOrder equiv'. \ No newline at end of file
diff --git a/test-suite/bugs/closed/4656.v b/test-suite/bugs/closed/4656.v
new file mode 100644
index 000000000..c89a86d63
--- /dev/null
+++ b/test-suite/bugs/closed/4656.v
@@ -0,0 +1,4 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+Goal True.
+ constructor 1.
+Qed.
diff --git a/test-suite/success/Compat84.v b/test-suite/success/Compat84.v
new file mode 100644
index 000000000..db6348fa1
--- /dev/null
+++ b/test-suite/success/Compat84.v
@@ -0,0 +1,19 @@
+(* -*- coq-prog-args: ("-emacs" "-compat" "8.4") -*- *)
+
+Goal True.
+ solve [ constructor 1 ]. Undo.
+ solve [ econstructor 1 ]. Undo.
+ solve [ constructor ]. Undo.
+ solve [ econstructor ]. Undo.
+ solve [ constructor (fail) ]. Undo.
+ solve [ econstructor (fail) ]. Undo.
+ split.
+Qed.
+
+Goal False \/ True.
+ solve [ constructor (constructor) ]. Undo.
+ solve [ econstructor (econstructor) ]. Undo.
+ solve [ constructor 2; constructor ]. Undo.
+ solve [ econstructor 2; econstructor ]. Undo.
+ right; esplit.
+Qed.
diff --git a/theories/Compat/Coq84.v b/theories/Compat/Coq84.v
index 90083b00d..5c60966f2 100644
--- a/theories/Compat/Coq84.v
+++ b/theories/Compat/Coq84.v
@@ -15,21 +15,28 @@ Ltac omega := Coq.omega.Omega.omega.
(** The number of arguments given in [match] statements has changed from 8.4 to 8.5. *)
Global Set Asymmetric Patterns.
+(** The automatic elimination schemes for records were dropped by default in 8.5. This restores the default behavior of Coq 8.4. *)
+Global Set Nonrecursive Elimination Schemes.
+
(** See bug 3545 *)
Global Set Universal Lemma Under Conjunction.
-(** In 8.5, [refine] leaves over dependent subgoals. *)
-Tactic Notation "refine" uconstr(term) := refine term; shelve_unifiable.
-
(** In 8.4, [constructor (tac)] allowed backtracking across the use of [constructor]; it has been subsumed by [constructor; tac]. *)
-Ltac constructor_84 := constructor.
Ltac constructor_84_n n := constructor n.
Ltac constructor_84_tac tac := once (constructor; tac).
-Tactic Notation "constructor" := constructor_84.
+Tactic Notation "constructor" := Coq.Init.Notations.constructor.
Tactic Notation "constructor" int_or_var(n) := constructor_84_n n.
Tactic Notation "constructor" "(" tactic(tac) ")" := constructor_84_tac tac.
+(** In 8.4, [econstructor (tac)] allowed backtracking across the use of [econstructor]; it has been subsumed by [econstructor; tac]. *)
+Ltac econstructor_84_n n := econstructor n.
+Ltac econstructor_84_tac tac := once (econstructor; tac).
+
+Tactic Notation "econstructor" := Coq.Init.Notations.econstructor.
+Tactic Notation "econstructor" int_or_var(n) := econstructor_84_n n.
+Tactic Notation "econstructor" "(" tactic(tac) ")" := econstructor_84_tac tac.
+
(** Some tactic notations do not factor well with tactics; we add global parsing entries for some tactics that would otherwise be overwritten by custom variants. See https://coq.inria.fr/bugs/show_bug.cgi?id=4392. *)
Tactic Notation "reflexivity" := reflexivity.
Tactic Notation "assumption" := assumption.
@@ -45,8 +52,6 @@ Tactic Notation "left" := left.
Tactic Notation "eleft" := eleft.
Tactic Notation "right" := right.
Tactic Notation "eright" := eright.
-Tactic Notation "constructor" := constructor.
-Tactic Notation "econstructor" := econstructor.
Tactic Notation "symmetry" := symmetry.
Tactic Notation "split" := split.
Tactic Notation "esplit" := esplit.
@@ -71,3 +76,11 @@ End Coq.
(** Many things now import [PeanoNat] rather than [NPeano], so we require it so that the old absolute names in [NPeano.Nat] are available. *)
Require Coq.Numbers.Natural.Peano.NPeano.
+
+(** The following coercions were declared by default in Specif.v. *)
+Coercion sig_of_sig2 : sig2 >-> sig.
+Coercion sigT_of_sigT2 : sigT2 >-> sigT.
+Coercion sigT_of_sig : sig >-> sigT.
+Coercion sig_of_sigT : sigT >-> sig.
+Coercion sigT2_of_sig2 : sig2 >-> sigT2.
+Coercion sig2_of_sigT2 : sigT2 >-> sig2.
diff --git a/toplevel/classes.ml b/toplevel/classes.ml
index 2fc0f5ff1..235732b52 100644
--- a/toplevel/classes.ml
+++ b/toplevel/classes.ml
@@ -121,7 +121,7 @@ let declare_instance_constant k pri global imps ?hook id pl poly evm term termty
instance_hook k pri global imps ?hook (ConstRef kn);
id
-let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) props
+let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) poly ctx (instid, bk, cl) props
?(generalize=true)
?(tac:unit Proofview.tactic option) ?hook pri =
let env = Global.env() in
@@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) poly ctx (instid, bk, cl) pro
if not (Evd.has_undefined evm) && not (Option.is_empty term) then
declare_instance_constant k pri global imps ?hook id pl
poly evm (Option.get term) termtype
- else if Flags.is_program_mode () || !refine_instance || Option.is_empty term then begin
+ else if Flags.is_program_mode () || refine || Option.is_empty term then begin
let kind = Decl_kinds.Global, poly, Decl_kinds.DefinitionBody Decl_kinds.Instance in
if Flags.is_program_mode () then
let hook vis gr _ =
diff --git a/toplevel/classes.mli b/toplevel/classes.mli
index a3e948d96..7beb873e6 100644
--- a/toplevel/classes.mli
+++ b/toplevel/classes.mli
@@ -40,6 +40,7 @@ val declare_instance_constant :
val new_instance :
?abstract:bool -> (** Not abstract by default. *)
?global:bool -> (** Not global by default. *)
+ ?refine:bool -> (** Allow refinement *)
Decl_kinds.polymorphic ->
local_binder list ->
typeclass_constraint ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 03:28:48 +0000