Merge PR coq#19016: Automatically register induction schemes from Scheme

Reviewed-by: ppedrot
Co-authored-by: ppedrot <[email protected]>

doc/changelog/08-vernac-commands-and-options/19016-scheme-auto-register.rst

@@ -0,0 +1,5 @@
+- **Changed:**
+  :cmd:`Scheme` automatically registers the resulting schemes in the :cmd:`Register Scheme` database
+  (`#19016 <https://github.com/coq/coq/pull/19016>`_,
+  fixes `#3132 <https://github.com/coq/coq/issues/3132>`_,
+  by Gaëtan Gilbert).

tactics/ind_tables.ml

@@ -73,6 +73,8 @@ let declare_individual_scheme_object key ?suff ?deps f =
 
 let is_declared_scheme_object key = Hashtbl.mem scheme_object_table key
 
+let scheme_kind_name (key : _ scheme_kind) : string = key
+
 (**********************************************************************)
 (* Defining/retrieving schemes *)
 

tactics/ind_tables.mli

@@ -59,6 +59,9 @@ val declare_individual_scheme_object : string ->
 val is_declared_scheme_object : string -> bool
 (** Is the string used as the name of a [scheme_kind]? *)
 
+val scheme_kind_name : _ scheme_kind -> string
+(** Name of a [scheme_kind]. Can be used to register with DeclareScheme. *)
+
 (** Force generation of a (mutually) scheme with possibly user-level names *)
 
 val define_individual_scheme : ?loc:Loc.t -> individual scheme_kind ->

test-suite/bugs/bug_3132.v

@@ -0,0 +1,36 @@
+Unset Elimination Schemes.
+Inductive eq (A:Type) (x:A) : A -> Prop :=
+    eq_refl : x = x :>A
+
+where "x = y :> A" := (@ eq A x y) : type_scope.
+
+Notation "x = y" := (x = y :>_) : type_scope.
+Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
+Notation "x <> y" := (x <> y :>_) : type_scope.
+
+Arguments eq {A} x _.
+Arguments eq_refl {A x} , [A] x.
+Set Elimination Schemes.
+
+Scheme eq_rect := Minimality for eq Sort Type.
+Scheme eq_rec := Minimality for eq Sort Set.
+Scheme eq_ind := Minimality for eq Sort Prop.
+
+(* needed for discriminate to recognize the hypothesis *)
+Register eq as core.eq.type.
+Register eq_refl as core.eq.refl.
+Register eq_ind as core.eq.ind.
+Register eq_rect as core.eq.rect.
+
+Lemma foo (H : true = false) : False.
+Proof.
+  discriminate.
+Defined.
+Print foo.
+
+Goal False.
+  let c := eval cbv delta [foo] in foo in
+    match c with
+      context[eq_ind] => idtac
+    end.
+Abort.

vernac/indschemes.ml

@@ -380,7 +380,6 @@ let rec name_and_process_schemes env l =
       (newref, sch_isdep sch_type, ind, sch_sort) :: name_and_process_schemes env q
 
 let do_mutual_induction_scheme ?(force_mutual=false) env l =
-  let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) l in
 
   let sigma, lrecspec, _ =
     List.fold_right
@@ -406,14 +405,17 @@ let do_mutual_induction_scheme ?(force_mutual=false) env l =
     let _,_,ind,_ = List.hd l in
     Global.is_polymorphic (Names.GlobRef.IndRef ind)
   in
-  let declare decl fi lrecref =
+  let declare decl ({CAst.v=fi},dep,ind,sort) =
     let decltype = Retyping.get_type_of env sigma decl in
     let decltype = EConstr.to_constr sigma decltype in
     let decl = EConstr.to_constr sigma decl in
     let cst = define ~poly fi sigma decl (Some decltype) in
-    Names.GlobRef.ConstRef cst :: lrecref
+    DeclareScheme.declare_scheme
+      (Ind_tables.scheme_kind_name @@ Elimschemes.elim_scheme ~dep ~to_kind:sort)
+      (ind,cst)
   in
-  let _ = List.fold_right2 declare listdecl lrecnames [] in
+  let () = List.iter2 declare listdecl l in
+  let lrecnames = List.map (fun ({CAst.v},_,_,_) -> v) l in
   Declare.fixpoint_message None lrecnames
 
 let do_scheme env l =