From 9afe18c3190bb0210e03bf40f3af101a7c5604da Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 20 Sep 2018 13:32:08 +0200
Subject: Scheme Equality: support for working in a context of Parameters.

It was working in very specific context of section variables. We make
it work similarly in the same kind of specific context of
Parameters. See test file SchemeEquality.v for the expected form. See
discussion at PR #8509.
---
 test-suite/success/SchemeEquality.v | 22 ++++++++++++++++++++++
 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")
-- 
cgit v1.2.3