Problem with ssreflect tuple

[Ptival]

The following:

From mathcomp Require Import tuple.

From Ornamental Require Import Ornaments.

Set DEVOID search prove equivalence. (* <-- Correctness proofs for search *)
Set DEVOID lift type. (* <-- Prettier types than the ones Coq infers *)

Module M.
  Definition mytuple := cons_tuple.
End M.

Preprocess Module M as M'.

raises error:

Error:
Cannot find the elimination combinator tuple_of_rect, the elimination of the inductive definition tuple_of on sort
Type is probably not allowed.

But I can't find a way of makingtuple_of opaque. I have tried:

Preprocess Module M as M' { opaque ssreflect.tuple.tuple_of }.

but it raises:

Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/.

Even though ssreflect.tuple.tuple_of is a qualified path in scope.

[tlringer]

Correct solution for this particular instance is to use Scheme Induction first, but I will look into why setting it as opaque raises a Not_found, and into better error messaging for the Scheme Induction problem.

[Ptival]

Cool, adding the following solved it:

Scheme Induction for tuple_of Sort Prop.
Scheme Induction for tuple_of Sort Set.
Scheme Induction for tuple_of Sort Type.

Scheme Induction for eqtype.Sub_spec Sort Prop.
Scheme Induction for eqtype.Sub_spec Sort Set.
Scheme Induction for eqtype.Sub_spec Sort Type.

Scheme Induction for eqtype.Equality.type Sort Prop.
Scheme Induction for eqtype.Equality.type Sort Set.
Scheme Induction for eqtype.Equality.type Sort Type.

Scheme Induction for eqtype.Equality.mixin_of Sort Prop.
Scheme Induction for eqtype.Equality.mixin_of Sort Set.
Scheme Induction for eqtype.Equality.mixin_of Sort Type.

Scheme Induction for eqtype.subType Sort Prop.
Scheme Induction for eqtype.subType Sort Set.
Scheme Induction for eqtype.subType Sort Type.