Traversal of inductive defs in Print Assumptions

This patch implements the traversal of inductive definitions in the
traverse function of toplevel/assumptions.ml which recursively
collects references in terms. In my opinion, this fixes a bug (but it
could be argued that inductive definitions were not traversed on
purpose). I think that is not possible to use this bug to hide a
meaningful use of an axiom.

You can try the patch with the following coq script:
Axiom n1 : nat.
Axiom n2 : nat.
Axiom n3 : nat.

Inductive I1 (p := n1) : Type := c1.
Inductive I2 : let p := n2 in Type := c2.
Inductive I3 : Type := c3 : let p := n3 in I3.

Inductive J : I1 -> I2 -> I3 -> Type :=
  | cj : J c1 c2 c3.
Inductive K : I1 -> I2 -> I3 -> Type := .

Definition T := I1 -> I2 -> I3.
Definition C := c1.

Print Assumptions I1.
Print Assumptions I2.
Print Assumptions I3.
Print Assumptions J.
Print Assumptions K.
Print Assumptions T.
Print Assumptions C.
Print Assumptions c1.
Print Assumptions c2.
Print Assumptions c3.
Print Assumptions cj.

The patch is a bit more complicated that I would have liked due to
the feature introduced in commit 2defd4c. Since this commit,
Print Assumptions also displays the type proved when one destruct
an axiom inhabiting an empty type. This provides more information
about where the old implementation of the admit tactic is used.
I am not a big fan of this feature, especially since the change in
the admit tactic.

PS: In order to write some tests, I had to change the criteria for
picking which axiom destruction are printed. The original
criteria was :
| Case (_,oty,c,[||]) ->
    (* non dependent match on an inductive with no constructor *)
    begin match Constr.(kind oty, kind c) with
     | Lambda(Anonymous,_,oty), Const (kn, _)
        when Vars.noccurn 1 oty &&
         not (Declareops.constant_has_body (lookup_constant kn)) ->
and I replaced Anonymous by _. Indeed, an Anonymous name here could
only be built using the "case" tactic and the pretyper seems to always
provide a name when compiling "match axiom as _ with end". And I
wanted to test what happened when this destruction occurs in
inductive definitions (which is of course weird in practice), for
instance:
Inductive I4 (X : Type) (p := match absurd return X with end)
     : Type -> Type :=
  c4 : forall (q := match absurd return X with end)
   (Y : Type) (r := match absurd return Y with end), I4 X Y.

The ability of "triggering" the display of this information only when
using the "case" tactic (and not destruct or pattern matching written
by hand) could have been a feature. If so, please feel free to
change back the criteria to "Anonymous".

0 files changed, 0 insertions, 0 deletions