diff options
| -rw-r--r-- | test-suite/success/SchemeEquality.v | 22 | ||||
| -rw-r--r-- | vernac/auto_ind_decl.ml | 15 |
2 files changed, 34 insertions, 3 deletions
diff --git a/test-suite/success/SchemeEquality.v b/test-suite/success/SchemeEquality.v index 00e84bff38..85d5c3e123 100644 --- a/test-suite/success/SchemeEquality.v +++ b/test-suite/success/SchemeEquality.v @@ -5,3 +5,25 @@ Definition N := nat. Inductive list := nil | cons : N -> list -> list. Scheme Equality for list. End A. + +Module B. + Section A. + Context A (eq_A:A->A->bool) + (A_bl : forall x y, eq_A x y = true -> x = y) + (A_lb : forall x y, x = y -> eq_A x y = true). + Inductive I := C : A -> I. + Scheme Equality for I. + End A. +End B. + +Module C. + Parameter A : Type. + Parameter eq_A : A->A->bool. + Parameter A_bl : forall x y, eq_A x y = true -> x = y. + Parameter A_lb : forall x y, x = y -> eq_A x y = true. + Hint Resolve A_bl A_lb : core. + Inductive I := C : A -> I. + Scheme Equality for I. + Inductive J := D : list A -> J. + Scheme Equality for J. +End C. diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 2013f19dc5..eb51d2341a 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -200,6 +200,7 @@ let build_beq_scheme mode kn = match Constr.kind c with | Rel x -> mkRel (x-nlist+ndx), Safe_typing.empty_private_constants | Var x -> + (* Support for working in a context with "eq_x : x -> x -> bool" *) let eid = Id.of_string ("eq_"^(Id.to_string x)) in let () = try ignore (Environ.lookup_named eid env) @@ -232,9 +233,17 @@ let build_beq_scheme mode kn = | Lambda _-> raise (EqUnknown "abstraction") | LetIn _ -> raise (EqUnknown "let-in") | Const (kn, u) -> - (match Environ.constant_opt_value_in env (kn, u) with - | None -> raise (ParameterWithoutEquality (ConstRef kn)) - | Some c -> aux (Term.applist (c,a))) + (match Environ.constant_opt_value_in env (kn, u) with + | Some c -> aux (Term.applist (c,a)) + | None -> + (* Support for working in a context with "eq_x : x -> x -> bool" *) + (* Needs Hints, see test suite *) + let eq_lbl = Label.make ("eq_" ^ Label.to_string (Constant.label kn)) in + let kneq = Constant.change_label kn eq_lbl in + try let _ = Environ.constant_opt_value_in env (kneq, u) in + Term.applist (mkConst kneq,a), + Safe_typing.empty_private_constants + with Not_found -> raise (ParameterWithoutEquality (ConstRef kn))) | Proj _ -> raise (EqUnknown "projection") | Construct _ -> raise (EqUnknown "constructor") | Case _ -> raise (EqUnknown "match") |