aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--CHANGES2
-rw-r--r--pretyping/pretype_errors.ml2
-rw-r--r--pretyping/pretype_errors.mli2
-rw-r--r--pretyping/unification.ml29
-rw-r--r--pretyping/unification.mli1
-rw-r--r--proofs/clenvtac.ml1
-rw-r--r--tactics/auto.ml3
-rw-r--r--tactics/class_tactics.ml4130
-rw-r--r--tactics/equality.ml24
-rw-r--r--tactics/setoid_replace.ml8
-rw-r--r--tactics/tactics.ml1
-rw-r--r--test-suite/bugs/closed/shouldsucceed/121.v17
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1425.v13
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1604.v7
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1683.v42
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1696.v16
-rw-r--r--test-suite/bugs/closed/shouldsucceed/1738.v30
-rw-r--r--test-suite/bugs/opened/shouldnotfail/1596.v242
-rw-r--r--test-suite/bugs/opened/shouldnotfail/1811.v9
-rw-r--r--theories/Classes/Morphisms.v6
-rw-r--r--toplevel/himsg.ml9
21 files changed, 508 insertions, 86 deletions
diff --git a/CHANGES b/CHANGES
index 1c3fe7b4c..7a9209af1 100644
--- a/CHANGES
+++ b/CHANGES
@@ -209,7 +209,7 @@ Setoid rewriting
and declare morphisms.
- "-->", "++>" and "==>" are now right associative notations
- declared at level 55 in scope signature_scope.
+ declared at level 90 in scope signature_scope.
Their introduction may break existing scripts that defined
them as notations with different levels.
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index f19dd1f97..cd32ac450 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -31,7 +31,7 @@ type pretype_error =
| CannotUnifyLocal of constr * constr * constr
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
- | NoOccurrenceFound of constr
+ | NoOccurrenceFound of constr * identifier option
(* Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index fbee6e04d..c6527f337 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -33,7 +33,7 @@ type pretype_error =
| CannotUnifyLocal of constr * constr * constr
| CannotUnifyBindingType of constr * constr
| CannotGeneralize of constr
- | NoOccurrenceFound of constr
+ | NoOccurrenceFound of constr * identifier option
(* Pretyping *)
| VarNotFound of identifier
| UnexpectedType of constr * constr
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index b1a4c3b8c..f11ed36da 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -96,13 +96,6 @@ let solve_pattern_eqn_array env f l c (metasubst,evarsubst) =
metasubst,(ev,solve_pattern_eqn env (Array.to_list l) c)::evarsubst
| _ -> assert false
-let expand_constant env predcst c =
- let (ids,csts) = Conv_oracle.freeze() in
- match kind_of_term c with
- | Const cst when Cpred.mem cst csts && Cpred.mem cst predcst -> constant_opt_value env cst
- | Var id when Idpred.mem id ids -> named_body id env
- | _ -> None
-
(*******************************)
(* Unification à l'ordre 0 de m et n: [unify_0 env sigma cv_pb m n]
@@ -127,20 +120,30 @@ type unify_flags = {
modulo_conv_on_closed_terms : bool;
use_metas_eagerly : bool;
modulo_delta : Cpred.t;
+ modulo_zeta : bool;
}
let default_unify_flags = {
modulo_conv_on_closed_terms = true;
use_metas_eagerly = true;
modulo_delta = Cpred.full;
+ modulo_zeta = true;
}
let default_no_delta_unify_flags = {
modulo_conv_on_closed_terms = true;
use_metas_eagerly = true;
modulo_delta = Cpred.empty;
+ modulo_zeta = true;
}
+let expand_constant env flags c =
+ let (ids,csts) = Conv_oracle.freeze() in
+ match kind_of_term c with
+ | Const cst when Cpred.mem cst csts && Cpred.mem cst flags.modulo_delta -> constant_opt_value env cst
+ | Var id when flags.modulo_zeta && Idpred.mem id ids -> named_body id env
+ | _ -> None
+
let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
let nb = nb_rel env in
let trivial_unify pb (metasubst,_) m n =
@@ -222,11 +225,11 @@ let unify_0_with_initial_metas metas conv_at_top env sigma cv_pb flags m n =
and expand curenv pb b substn cM f1 l1 cN f2 l2 =
if trivial_unify pb substn cM cN then substn
else if b & not (Cpred.is_empty flags.modulo_delta) then
- match expand_constant curenv flags.modulo_delta f1 with
+ match expand_constant curenv flags f1 with
| Some c ->
unirec_rec curenv pb b substn (whd_betaiotazeta (mkApp(c,l1))) cN
| None ->
- match expand_constant curenv flags.modulo_delta f2 with
+ match expand_constant curenv flags f2 with
| Some c ->
unirec_rec curenv pb b substn cM (whd_betaiotazeta (mkApp(c,l2)))
| None ->
@@ -608,7 +611,7 @@ let w_unify_to_subterm env ?(flags=default_unify_flags) (op,cl) evd =
in
try matchrec cl
with ex when precatchable_exception ex ->
- raise (PretypeError (env,NoOccurrenceFound op))
+ raise (PretypeError (env,NoOccurrenceFound (op, None)))
let w_unify_to_subterm_list env flags allow_K oplist t evd =
List.fold_right
@@ -628,7 +631,7 @@ let w_unify_to_subterm_list env flags allow_K oplist t evd =
(evd,op::l)
else
(* This is not up to delta ... *)
- raise (PretypeError (env,NoOccurrenceFound op)))
+ raise (PretypeError (env,NoOccurrenceFound (op, None))))
oplist
(evd,[])
@@ -693,7 +696,7 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
with ex when precatchable_exception ex ->
try
w_unify2 env flags allow_K cv_pb ty1 ty2 evd
- with PretypeError (env,NoOccurrenceFound c) as e -> raise e
+ with PretypeError (env,NoOccurrenceFound _) as e -> raise e
| ex when precatchable_exception ex ->
error "Cannot solve a second-order unification problem")
@@ -701,7 +704,7 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
| (Meta _, true, _, _ | _, _, Meta _, true) ->
(try
w_unify2 env flags allow_K cv_pb ty1 ty2 evd
- with PretypeError (env,NoOccurrenceFound c) as e -> raise e
+ with PretypeError (env,NoOccurrenceFound _) as e -> raise e
| ex when precatchable_exception ex ->
try
w_typed_unify env cv_pb flags ty1 ty2 evd
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index e0551b625..8e8168e5c 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -18,6 +18,7 @@ type unify_flags = {
modulo_conv_on_closed_terms : bool;
use_metas_eagerly : bool;
modulo_delta : Names.Cpred.t;
+ modulo_zeta : bool;
}
val default_unify_flags : unify_flags
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 60abc5d66..c966e876f 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -99,6 +99,7 @@ let fail_quick_unif_flags = {
modulo_conv_on_closed_terms = true;
use_metas_eagerly = false;
modulo_delta = Cpred.empty;
+ modulo_zeta = true;
}
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 52c483771..00d7b8cb4 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -567,7 +567,8 @@ open Unification
let auto_unif_flags = {
modulo_conv_on_closed_terms = true;
use_metas_eagerly = false;
- modulo_delta = Cpred.empty;
+ modulo_delta = Cpred.empty;
+ modulo_zeta = true;
}
(* Try unification with the precompiled clause, then use registered Apply *)
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 685f11d47..f56089b1e 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -40,6 +40,19 @@ open Command
open Libnames
open Evd
+let check_required_library d =
+ let d' = List.map id_of_string d in
+ let dir = make_dirpath (List.rev d') in
+ if (* not (Library.library_is_opened dir) || *)not (Library.library_is_loaded dir) then
+ error ("Library "^(list_last d)^" has to be required first")
+
+let classes_dirpath =
+ make_dirpath (List.map id_of_string ["Classes";"Coq"])
+
+let init_setoid () =
+ if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
+ else check_required_library ["Coq";"Setoids";"Setoid"]
+
(** Typeclasses instance search tactic / eauto *)
open Auto
@@ -58,6 +71,7 @@ let auto_unif_flags = ref {
modulo_conv_on_closed_terms = true;
use_metas_eagerly = true;
modulo_delta = Cpred.empty;
+ modulo_zeta = true;
}
let unify_e_resolve (c,clenv) gls =
@@ -409,6 +423,7 @@ let init () =
modulo_conv_on_closed_terms = true;
use_metas_eagerly = true;
modulo_delta = Cpred.empty;
+ modulo_zeta = true;
}
let _ =
@@ -642,6 +657,7 @@ let resolve_morphism env sigma oldt m ?(fnewt=fun x -> x) args args' cstr evars
type hypinfo = {
cl : clausenv;
prf : constr;
+ car : constr;
rel : constr;
l2r : bool;
c1 : constr;
@@ -650,31 +666,44 @@ type hypinfo = {
abs : (constr * types) option;
}
+let convertible env evd x y =
+ try ignore(Evarconv.the_conv_x env x y evd); true
+ with _ -> false
+ (* ignore(Reduction.conv env x y) *)
+
let decompose_setoid_eqhyp env sigma c left2right =
let ctype = Typing.type_of env sigma c in
- let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ctype) in
+ let eqclause = Clenv.mk_clenv_from_env env sigma None (c,ctype) in
let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
let rec split_last_two = function
| [c1;c2] -> [],(c1, c2)
| x::y::z ->
let l,res = split_last_two (y::z) in x::l, res
| _ -> error "The term provided is not an applied relation" in
- let others, (c1,c2) = split_last_two args in
- { cl=eqclause; prf=(Clenv.clenv_value eqclause);
- rel=mkApp (equiv, Array.of_list others);
- l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
+ let others,(c1,c2) = split_last_two args in
+ let ty1, ty2 =
+ Typing.mtype_of env eqclause.evd c1, Typing.mtype_of env eqclause.evd c2
+ in
+ if not (convertible env eqclause.evd ty1 ty2) then
+ error "The term does not end with an applied homogeneous relation"
+ else
+ { cl=eqclause; prf=(Clenv.clenv_value eqclause);
+ car=ty1; rel=mkApp (equiv, Array.of_list others);
+ l2r=left2right; c1=c1; c2=c2; c=Some c; abs=None }
let rewrite_unif_flags = {
Unification.modulo_conv_on_closed_terms = false;
Unification.use_metas_eagerly = true;
- Unification.modulo_delta = Cpred.empty
+ Unification.modulo_delta = Cpred.empty;
+ Unification.modulo_zeta = false;
}
let rewrite2_unif_flags = {
Unification.modulo_conv_on_closed_terms = true;
Unification.use_metas_eagerly = true;
- Unification.modulo_delta = Cpred.empty
- }
+ Unification.modulo_delta = Cpred.empty;
+ Unification.modulo_zeta = false;
+}
(* let unification_rewrite c1 c2 cl but gl = *)
(* let (env',c1) = *)
@@ -707,27 +736,39 @@ let refresh_hypinfo env sigma hypinfo =
| _ -> ()
else ()
-let convertible env x y =
- ignore(Reduction.conv env x y)
-
let unify_eqn env sigma hypinfo t =
try
- let {cl=cl; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
- let env' =
+ let {cl=cl; prf=prf; car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=c; abs=abs} = !hypinfo in
+ let env', c1, c2, car, rel =
match abs with
- Some _ -> convertible env (if l2r then c1 else c2) t; cl
+ Some _ ->
+ if convertible env cl.evd (if l2r then c1 else c2) t then
+ cl, c1, c2, car, rel
+ else raise Not_found
| None ->
- try clenv_unify allowK ~flags:rewrite_unif_flags
- CONV (if l2r then c1 else c2) t cl
- with Pretype_errors.PretypeError _ ->
- (* For Ring essentially, only when doing setoid_rewrite *)
- clenv_unify allowK ~flags:rewrite2_unif_flags
+ let env' =
+ try clenv_unify allowK ~flags:rewrite_unif_flags
CONV (if l2r then c1 else c2) t cl
+ with Pretype_errors.PretypeError _ ->
+ (* For Ring essentially, only when doing setoid_rewrite *)
+ clenv_unify allowK ~flags:rewrite2_unif_flags
+ CONV (if l2r then c1 else c2) t cl
+ in
+ let env' =
+ let mvs = clenv_dependent false env' in
+ clenv_pose_metas_as_evars env' mvs
+ in
+ let c1 = Clenv.clenv_nf_meta env' c1
+ and c2 = Clenv.clenv_nf_meta env' c2
+ and car = Clenv.clenv_nf_meta env' car
+ and rel = Clenv.clenv_nf_meta env' rel in
+ let ty1 = Typing.mtype_of env'.env env'.evd c1
+ and ty2 = Typing.mtype_of env'.env env'.evd c2
+ in
+ if convertible env env'.evd ty1 ty2 then
+ env', c1, c2, car, rel
+ else raise Not_found
in
- let c1 = Clenv.clenv_nf_meta env' c1
- and c2 = Clenv.clenv_nf_meta env' c2
- and rel = Clenv.clenv_nf_meta env' rel in
- let car = Typing.type_of env'.env (Evd.evars_of env'.evd) c1 in
let prf =
if abs = None then
(* let (rel, args) = destApp typ in *)
@@ -747,7 +788,7 @@ let unify_eqn env sigma hypinfo t =
in Some (env', res)
with _ -> None
-let unfold_impl t =
+let unfold_impl t =
match kind_of_term t with
| App (arrow, [| a; b |])(* when eq_constr arrow (Lazy.force impl) *) ->
mkProd (Anonymous, a, b)
@@ -813,7 +854,7 @@ let build_new gl env sigma flags occs hypinfo concl cstr evars =
let rec aux env t occ cstr =
match unify_eqn env sigma hypinfo t with
| Some (env', (prf, hypinfo as x)) ->
- if is_occ occ then (
+ if is_occ occ then (
evars := Evd.evar_merge !evars (Evd.evars_of (Evd.undefined_evars env'.evd));
match cstr with
None -> Some x, succ occ
@@ -971,16 +1012,19 @@ let cl_rewrite_clause_aux ?(flags=default_flags) hypinfo goal_meta occs clause g
in tclTHENLIST [evartac; rewtac] gl
with
| TypeClassError (env, (UnsatisfiableConstraints _ as e)) ->
- tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints."
- ++ Himsg.explain_typeclass_error env e) gl
- | Not_found ->
- tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl)
+ tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints."
+ ++ fnl () ++ Himsg.explain_typeclass_error env e) gl)
+(* | Not_found -> *)
+(* tclFAIL 0 (str" setoid rewrite failed: unable to satisfy the rewriting constraints.") gl) *)
| None ->
let {l2r=l2r; c1=x; c2=y} = !hypinfo in
- raise (Pretype_errors.PretypeError (pf_env gl, Pretype_errors.NoOccurrenceFound (if l2r then x else y)))
+ raise (Pretype_errors.PretypeError
+ (pf_env gl,
+ Pretype_errors.NoOccurrenceFound ((if l2r then x else y), is_hyp)))
(* tclFAIL 1 (str"setoid rewrite failed") gl *)
let cl_rewrite_clause c left2right occs clause gl =
+ init_setoid ();
let meta = Evarutil.new_meta() in
let hypinfo = ref (decompose_setoid_eqhyp (pf_env gl) (project gl) c left2right) in
cl_rewrite_clause_aux hypinfo meta occs clause gl
@@ -1114,15 +1158,6 @@ let require_library dirpath =
let qualid = (dummy_loc, Libnames.qualid_of_dirpath (Libnames.dirpath_of_string dirpath)) in
Library.require_library [qualid] (Some false)
-let check_required_library d =
- let d' = List.map id_of_string d in
- let dir = make_dirpath (List.rev d') in
- if (* not (Library.library_is_opened dir) || *)not (Library.library_is_loaded dir) then
- error ("Library "^(list_last d)^" has to be required first")
-
-let init_setoid () =
- check_required_library ["Coq";"Setoids";"Setoid"]
-
let declare_instance_refl binders a aeq n lemma =
let instance = declare_instance a aeq (add_suffix n "_Reflexive") "Coq.Classes.RelationClasses.Reflexive"
in anew_instance binders instance
@@ -1435,7 +1470,7 @@ let check_evar_map_of_evars_defs evd =
check_freemetas_is_empty rebus2 freemetas2
) metas
-let unification_rewrite l2r c1 c2 cl rel but gl =
+let unification_rewrite l2r c1 c2 cl car rel but gl =
let (env',c') =
try
(* ~flags:(false,true) to allow to mark occurrences that must not be
@@ -1456,7 +1491,7 @@ let unification_rewrite l2r c1 c2 cl rel but gl =
let prf = Clenv.clenv_value cl' in
let prfty = Clenv.clenv_type cl' in
let cl' = { cl' with templval = mk_freelisted prf ; templtyp = mk_freelisted prfty } in
- {cl=cl'; prf=(mkRel 1); rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
+ {cl=cl'; prf=(mkRel 1); car=car; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=Some (prf, prfty)}
(* if occur_meta prf then *)
(* else *)
(* {cl=cl'; prf=prf; rel=rel; l2r=l2r; c1=c1; c2=c2; c=None; abs=None} *)
@@ -1466,7 +1501,7 @@ let get_hyp gl c clause l2r =
Prod _ ->
let hi = decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r in
let but = match clause with Some id -> pf_get_hyp_typ gl id | None -> pf_concl gl in
- unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.rel but gl
+ unification_rewrite hi.l2r hi.c1 hi.c2 hi.cl hi.car hi.rel but gl
| _ -> decompose_setoid_eqhyp (pf_env gl) (project gl) c l2r
let general_rewrite_flags = { under_lambdas = false; on_morphisms = false }
@@ -1481,15 +1516,8 @@ let general_s_rewrite_in id l2r occs c ~new_goals gl =
let hypinfo = ref (get_hyp gl c (Some id) l2r) in
cl_rewrite_clause_aux ~flags:general_rewrite_flags hypinfo meta occs (Some (([],id), [])) gl
-let classes_dirpath =
- make_dirpath (List.map id_of_string ["Classes";"Coq"])
-
-let init_rewrite () =
- if is_dirpath_prefix_of classes_dirpath (Lib.cwd ()) then ()
- else check_required_library ["Coq";"Setoids";"Setoid"]
-
let general_s_rewrite_clause x =
- init_rewrite ();
+ init_setoid ();
match x with
| None -> general_s_rewrite
| Some id -> general_s_rewrite_in id
@@ -1511,7 +1539,7 @@ let is_loaded d =
Library.library_is_loaded dir
let try_loaded f gl =
- if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl
+ if is_loaded ["Coq";"Classes";"RelationClasses"] then f gl
else tclFAIL 0 (str"You need to require Coq.Classes.RelationClasses first") gl
let setoid_reflexivity gl =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f91845a5c..b8e868f37 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -52,15 +52,21 @@ open Indrec
*)
(* Ad hoc asymmetric general_elim_clause *)
-let general_elim_clause with_evars cls c elim = match cls with
- | None ->
- (* was tclWEAK_PROGRESS which only fails for tactics generating one
- subgoal and did not fail for useless conditional rewritings generating
- an extra condition *)
- tclNOTSAMEGOAL (general_elim with_evars c elim ~allow_K:false)
- | Some id ->
- general_elim_in with_evars id c elim
-
+let general_elim_clause with_evars cls c elim =
+ try
+ (match cls with
+ | None ->
+ (* was tclWEAK_PROGRESS which only fails for tactics generating one
+ subgoal and did not fail for useless conditional rewritings generating
+ an extra condition *)
+ tclNOTSAMEGOAL (general_elim with_evars c elim ~allow_K:false)
+ | Some id ->
+ general_elim_in with_evars id c elim)
+ with Pretype_errors.PretypeError (env,
+ (Pretype_errors.NoOccurrenceFound (c', _))) ->
+ raise (Pretype_errors.PretypeError
+ (env, (Pretype_errors.NoOccurrenceFound (c', cls))))
+
let elimination_sort_of_clause = function
| None -> elimination_sort_of_goal
| Some id -> elimination_sort_of_hyp id
diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 69840f85c..e3c4e2649 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1734,14 +1734,16 @@ let check_evar_map_of_evars_defs evd =
let rewrite_unif_flags = {
modulo_conv_on_closed_terms = false;
use_metas_eagerly = true;
- modulo_delta = Cpred.empty
+ modulo_delta = Cpred.empty;
+ modulo_zeta = false;
}
let rewrite2_unif_flags = {
modulo_conv_on_closed_terms = true;
use_metas_eagerly = true;
- modulo_delta = Cpred.empty
- }
+ modulo_delta = Cpred.empty;
+ modulo_zeta = false;
+}
let unification_rewrite c1 c2 cl but gl =
let (env',c1) =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c3f9c37e9..9eec0c064 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -552,6 +552,7 @@ let elim_flags = {
modulo_conv_on_closed_terms = true;
use_metas_eagerly = true;
modulo_delta = Cpred.empty;
+ modulo_zeta = true;
}
let elimination_clause_scheme with_evars allow_K elimclause indclause gl =
diff --git a/test-suite/bugs/closed/shouldsucceed/121.v b/test-suite/bugs/closed/shouldsucceed/121.v
new file mode 100644
index 000000000..d193aa73f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/121.v
@@ -0,0 +1,17 @@
+Require Import Setoid.
+
+Section Setoid_Bug.
+
+Variable X:Type -> Type.
+Variable Xeq : forall A, (X A) -> (X A) -> Prop.
+Hypothesis Xst : forall A, Equivalence (X A) (Xeq A).
+
+Variable map : forall A B, (A -> B) -> X A -> X B.
+
+Implicit Arguments map [A B].
+
+Goal forall A B (a b:X (B -> A)) (c:X A) (f:A -> B -> A), Xeq _ a b -> Xeq _ b (map f c) -> Xeq _ a (map f c).
+intros A B a b c f Hab Hbc.
+rewrite Hab.
+assumption.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1425.v b/test-suite/bugs/closed/shouldsucceed/1425.v
new file mode 100644
index 000000000..f5fbb8a2a
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1425.v
@@ -0,0 +1,13 @@
+Require Import Setoid.
+
+Parameter recursion : forall A : Set, A -> (nat -> A -> A) -> nat -> A.
+
+Axiom recursion_S :
+ forall (A : Set) (EA : relation A) (a : A) (f : nat -> A -> A) (n : nat),
+ EA (recursion A a f (S n)) (f n (recursion A a f n)).
+
+Goal forall n : nat, recursion nat 0 (fun _ _ => 1) (S n) = 1.
+intro n.
+setoid_rewrite recursion_S.
+reflexivity.
+Qed. \ No newline at end of file
diff --git a/test-suite/bugs/closed/shouldsucceed/1604.v b/test-suite/bugs/closed/shouldsucceed/1604.v
new file mode 100644
index 000000000..2d0991cb1
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1604.v
@@ -0,0 +1,7 @@
+Require Import Setoid.
+
+Parameter F : nat -> nat.
+Axiom F_id : forall n : nat, n = F n.
+Goal forall n : nat, F n = n.
+intro n. setoid_rewrite F_id at 2. reflexivity.
+Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1683.v b/test-suite/bugs/closed/shouldsucceed/1683.v
new file mode 100644
index 000000000..1571ee20e
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1683.v
@@ -0,0 +1,42 @@
+Require Import Setoid.
+
+Section SetoidBug.
+
+Variable ms : Type.
+Variable ms_type : ms -> Type.
+Variable ms_eq : forall (A:ms), relation (ms_type A).
+
+Variable CR : ms.
+
+Record Ring : Type :=
+{Ring_type : Type}.
+
+Variable foo : forall (A:Ring), nat -> Ring_type A.
+Variable IR : Ring.
+Variable IRasCR : Ring_type IR -> ms_type CR.
+
+Definition CRasCRing : Ring := Build_Ring (ms_type CR).
+
+Hypothesis ms_refl : forall A x, ms_eq A x x.
+Hypothesis ms_sym : forall A x y, ms_eq A x y -> ms_eq A y x.
+Hypothesis ms_trans : forall A x y z, ms_eq A x y -> ms_eq A y z -> ms_eq A x z.
+
+Add Parametric Relation A : (ms_type A) (ms_eq A)
+ reflexivity proved by (ms_refl A)
+ symmetry proved by (ms_sym A)
+ transitivity proved by (ms_trans A)
+ as ms_Setoid.
+
+Hypothesis foobar : forall n, ms_eq CR (IRasCR (foo IR n)) (foo CRasCRing n).
+
+Goal forall (b:ms_type CR),
+ ms_eq CR (IRasCR (foo IR O)) b ->
+ ms_eq CR (IRasCR (foo IR O)) b.
+intros b H.
+rewrite foobar.
+rewrite foobar in H.
+assumption.
+Qed.
+
+
+
diff --git a/test-suite/bugs/closed/shouldsucceed/1696.v b/test-suite/bugs/closed/shouldsucceed/1696.v
new file mode 100644
index 000000000..0826428a3
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1696.v
@@ -0,0 +1,16 @@
+Require Import Setoid.
+
+Inductive mynat := z : mynat | s : mynat -> mynat.
+
+Parameter E : mynat -> mynat -> Prop.
+Axiom E_equiv : equiv mynat E.
+
+Add Relation mynat E
+ reflexivity proved by (proj1 E_equiv)
+ symmetry proved by (proj2 (proj2 E_equiv))
+ transitivity proved by (proj1 (proj2 E_equiv))
+as E_rel.
+
+Notation "x == y" := (E x y) (at level 70).
+
+Goal z == s z -> s z == z. intros H. setoid_rewrite H at 2. reflexivity. Qed.
diff --git a/test-suite/bugs/closed/shouldsucceed/1738.v b/test-suite/bugs/closed/shouldsucceed/1738.v
new file mode 100644
index 000000000..0deed3663
--- /dev/null
+++ b/test-suite/bugs/closed/shouldsucceed/1738.v
@@ -0,0 +1,30 @@
+Require Import FSets.
+
+Module SomeSetoids (Import M:FSetInterface.S).
+
+Lemma Equal_refl : forall s, s[=]s.
+Proof. red; split; auto. Qed.
+
+Add Relation t Equal
+ reflexivity proved by Equal_refl
+ symmetry proved by eq_sym
+ transitivity proved by eq_trans
+ as EqualSetoid.
+
+Add Morphism Empty with signature Equal ==> iff as Empty_m.
+Proof.
+unfold Equal, Empty; firstorder.
+Qed.
+
+End SomeSetoids.
+
+Module Test (Import M:FSetInterface.S).
+ Module A:=SomeSetoids M.
+ Module B:=SomeSetoids M. (* lots of warning *)
+
+ Lemma Test : forall s s', s[=]s' -> Empty s -> Empty s'.
+ intros.
+ rewrite H in H0.
+ assumption.
+Qed.
+End Test. \ No newline at end of file
diff --git a/test-suite/bugs/opened/shouldnotfail/1596.v b/test-suite/bugs/opened/shouldnotfail/1596.v
new file mode 100644
index 000000000..766bf524c
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1596.v
@@ -0,0 +1,242 @@
+
+Require Import Relations.
+Require Import FSets.
+Require Import Arith.
+
+Lemma Bool_elim_bool : forall (b:bool),b=true \/ b=false.
+ destruct b;try tauto.
+Qed.
+
+Module OrderedPair (X:OrderedType) (Y:OrderedType) <: OrderedType with
+Definition t := (X.t * Y.t)%type.
+ Definition t := (X.t * Y.t)%type.
+
+ Definition eq (xy1:t) (xy2:t) :=
+ let (x1,y1) := xy1 in
+ let (x2,y2) := xy2 in
+ (X.eq x1 x2) /\ (Y.eq y1 y2).
+
+ Definition lt (xy1:t) (xy2:t) :=
+ let (x1,y1) := xy1 in
+ let (x2,y2) := xy2 in
+ (X.lt x1 x2) \/ ((X.eq x1 x2) /\ (Y.lt y1 y2)).
+
+ Lemma eq_refl : forall (x:t),(eq x x).
+ destruct x.
+ unfold eq.
+ split;[apply X.eq_refl | apply Y.eq_refl].
+ Qed.
+
+ Lemma eq_sym : forall (x y:t),(eq x y)->(eq y x).
+ destruct x;destruct y;unfold eq;intro.
+ elim H;clear H;intros.
+ split;[apply X.eq_sym | apply Y.eq_sym];trivial.
+ Qed.
+
+ Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
+ unfold eq;destruct x;destruct y;destruct z;intros.
+ elim H;clear H;intros.
+ elim H0;clear H0;intros.
+ split;[eapply X.eq_trans | eapply Y.eq_trans];eauto.
+ Qed.
+
+ Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
+ unfold lt;destruct x;destruct y;destruct z;intros.
+ case H;clear H;intro.
+ case H0;clear H0;intro.
+ left.
+ eapply X.lt_trans;eauto.
+ elim H0;clear H0;intros.
+ left.
+ case (X.compare t0 t4);trivial;intros.
+ generalize (X.eq_sym H0);intro.
+ generalize (X.eq_trans e H2);intro.
+ elim (X.lt_not_eq H H3).
+ generalize (X.lt_trans l H);intro.
+ generalize (X.eq_sym H0);intro.
+ elim (X.lt_not_eq H2 H3).
+ elim H;clear H;intros.
+ case H0;clear H0;intro.
+ left.
+ case (X.compare t0 t4);trivial;intros.
+ generalize (X.eq_sym H);intro.
+ generalize (X.eq_trans H2 e);intro.
+ elim (X.lt_not_eq H0 H3).
+ generalize (X.lt_trans H0 l);intro.
+ generalize (X.eq_sym H);intro.
+ elim (X.lt_not_eq H2 H3).
+ elim H0;clear H0;intros.
+ right.
+ split.
+ eauto.
+ eauto.
+ Qed.
+
+ Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
+ unfold lt, eq;destruct x;destruct y;intro;intro.
+ elim H0;clear H0;intros.
+ case H.
+ intro.
+ apply (X.lt_not_eq H2 H0).
+ intro.
+ elim H2;clear H2;intros.
+ apply (Y.lt_not_eq H3 H1).
+ Qed.
+
+ Definition compare : forall (x y:t),(Compare lt eq x y).
+ destruct x;destruct y.
+ case (X.compare t0 t2);intro.
+ apply LT.
+ left;trivial.
+ case (Y.compare t1 t3);intro.
+ apply LT.
+ right.
+ tauto.
+ apply EQ.
+ split;trivial.
+ apply GT.
+ right;auto.
+ apply GT.
+ left;trivial.
+ Defined.
+
+ Hint Immediate eq_sym.
+ Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
+End OrderedPair.
+
+Module MessageSpi.
+ Inductive message : Set :=
+ | MNam : nat -> message.
+
+ Definition t := message.
+
+ Fixpoint message_lt (m n:message) {struct m} : Prop :=
+ match (m,n) with
+ | (MNam n1,MNam n2) => n1 < n2
+ end.
+
+ Module Ord <: OrderedType with Definition t := message with Definition eq :=
+@eq message.
+ Definition t := message.
+ Definition eq := @eq message.
+ Definition lt := message_lt.
+
+ Lemma eq_refl : forall (x:t),eq x x.
+ unfold eq;auto.
+ Qed.
+
+ Lemma eq_sym : forall (x y:t),(eq x y )->(eq y x).
+ unfold eq;auto.
+ Qed.
+
+ Lemma eq_trans : forall (x y z:t),(eq x y)->(eq y z)->(eq x z).
+ unfold eq;auto;intros;congruence.
+ Qed.
+
+ Lemma lt_trans : forall (x y z:t),(lt x y)->(lt y z)->(lt x z).
+ unfold lt.
+ induction x;destruct y;simpl;try tauto;destruct z;try tauto;intros.
+ omega.
+ Qed.
+
+ Lemma lt_not_eq : forall (x y:t),(lt x y)->~(eq x y).
+ unfold eq;unfold lt.
+ induction x;destruct y;simpl;try tauto;intro;red;intro;try (discriminate
+H0);injection H0;intros.
+ elim (lt_irrefl n);try omega.
+ Qed.
+
+ Definition compare : forall (x y:t),(Compare lt eq x y).
+ unfold lt, eq.
+ induction x;destruct y;intros;try (apply LT;simpl;trivial;fail);try
+(apply
+GT;simpl;trivial;fail).
+ case (lt_eq_lt_dec n n0);intros;try (case s;clear s;intros).
+ apply LT;trivial.
+ apply EQ;trivial.
+ rewrite e;trivial.
+ apply GT;trivial.
+ Defined.
+
+ Hint Immediate eq_sym.
+ Hint Resolve eq_refl eq_trans lt_not_eq lt_trans.
+ End Ord.
+
+ Theorem eq_dec : forall (m n:message),{m=n}+{~(m=n)}.
+ intros.
+ case (Ord.compare m n);intro;[right | left | right];try (red;intro).
+ elim (Ord.lt_not_eq m n);auto.
+ rewrite e;auto.
+ elim (Ord.lt_not_eq n m);auto.
+ Defined.
+End MessageSpi.
+
+Module MessagePair := OrderedPair MessageSpi.Ord MessageSpi.Ord.
+
+Module Type Hedge := FSetInterface.S with Module E := MessagePair.
+
+Module A (H:Hedge).
+ Definition hedge := H.t.
+
+ Definition message_relation := relation MessageSpi.message.
+
+ Definition relation_of_hedge (h:hedge) (m n:MessageSpi.message) := H.In (m,n)
+h.
+
+ Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
+ | SynInc : forall (m n:MessageSpi.message),(h m
+n)->(hedge_synthesis_relation h m n).
+
+ Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.message)
+(n:MessageSpi.message) {struct m} : bool :=
+ if H.mem (m,n) h
+ then true
+ else false.
+
+ Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
+(relation_of_hedge h).
+
+ Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
+(m n:MessageSpi.message),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec
+h m n).
+ unfold hedge_synthesis_spec;unfold relation_of_hedge.
+ induction m;simpl;intro.
+ elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
+ apply SynInc;apply H.mem_2;trivial.
+ rewrite H in H0. (* !! possible here !! *)
+ discriminate H0.
+ Qed.
+End A.
+
+Module B (H:Hedge).
+ Definition hedge := H.t.
+
+ Definition message_relation := relation MessageSpi.t.
+
+ Definition relation_of_hedge (h:hedge) (m n:MessageSpi.t) := H.In (m,n) h.
+
+ Inductive hedge_synthesis_relation (h:message_relation) : message_relation :=
+ | SynInc : forall (m n:MessageSpi.t),(h m n)->(hedge_synthesis_relation h m
+n).
+
+ Fixpoint hedge_in_synthesis (h:hedge) (m:MessageSpi.t) (n:MessageSpi.t)
+{struct m} : bool :=
+ if H.mem (m,n) h
+ then true
+ else false.
+
+ Definition hedge_synthesis_spec (h:hedge) := hedge_synthesis_relation
+(relation_of_hedge h).
+
+ Lemma hedge_in_synthesis_impl_hedge_synthesis_spec : forall (h:hedge),forall
+(m n:MessageSpi.t),(hedge_in_synthesis h m n)=true->(hedge_synthesis_spec h m
+n).
+ unfold hedge_synthesis_spec;unfold relation_of_hedge.
+ induction m;simpl;intro.
+ elim (Bool_elim_bool (H.mem (MessageSpi.MNam n,n0) h));intros.
+ apply SynInc;apply H.mem_2;trivial.
+
+ rewrite H in H0. (* !! impossible here !! *)
+ discriminate H0.
+ Qed.
+End B. \ No newline at end of file
diff --git a/test-suite/bugs/opened/shouldnotfail/1811.v b/test-suite/bugs/opened/shouldnotfail/1811.v
new file mode 100644
index 000000000..037b7cb2d
--- /dev/null
+++ b/test-suite/bugs/opened/shouldnotfail/1811.v
@@ -0,0 +1,9 @@
+Require Export Bool.
+
+Lemma neg2xor : forall b, xorb true b = negb b.
+Proof. auto. Qed.
+
+Goal forall b1 b2, (negb b1 = b2) -> xorb true b1 = b2.
+Proof.
+ intros b1 b2.
+ rewrite neg2xor. \ No newline at end of file
diff --git a/theories/Classes/Morphisms.v b/theories/Classes/Morphisms.v
index e2d3f21c7..295d7d1a6 100644
--- a/theories/Classes/Morphisms.v
+++ b/theories/Classes/Morphisms.v
@@ -50,13 +50,13 @@ Definition respectful (A B : Type) (R : relation A) (R' : relation B) : relation
Delimit Scope signature_scope with signature.
Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
- (right associativity, at level 55) : signature_scope.
+ (right associativity, at level 90) : signature_scope.
Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
- (right associativity, at level 55) : signature_scope.
+ (right associativity, at level 90) : signature_scope.
Notation " R --> R' " := (@respectful _ _ (inverse (R%signature)) (R'%signature))
- (right associativity, at level 55) : signature_scope.
+ (right associativity, at level 90) : signature_scope.
Arguments Scope respectful [type_scope type_scope signature_scope signature_scope].
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 505f456db..4950f4064 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -406,9 +406,12 @@ let explain_refiner_cannot_generalize env ty =
str "Cannot find a well-typed generalisation of the goal with type : " ++
pr_lconstr_env env ty
-let explain_no_occurrence_found env c =
+let explain_no_occurrence_found env c id =
str "Found no subterm matching " ++ pr_lconstr_env env c ++
- str " in the current goal"
+ str " in " ++
+ (match id with
+ | Some id -> pr_id id
+ | None -> str"the current goal")
let explain_cannot_unify_binding_type env m n =
let pm = pr_lconstr_env env m in
@@ -465,7 +468,7 @@ let explain_pretype_error env err =
| CannotUnify (m,n) -> explain_cannot_unify env m n
| CannotUnifyLocal (m,n,sn) -> explain_cannot_unify_local env m n sn
| CannotGeneralize ty -> explain_refiner_cannot_generalize env ty
- | NoOccurrenceFound c -> explain_no_occurrence_found env c
+ | NoOccurrenceFound (c, id) -> explain_no_occurrence_found env c id
| CannotUnifyBindingType (m,n) -> explain_cannot_unify_binding_type env m n
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 22:00:33 +0000