Applicative commutative cuts in Fixpoint guard condition

In "(match ... with |... -> fun x -> t end) u", "x" has now the subterm
property of "u" in the analysis of "t".

Commutative cuts aren't compatible with typing so we need to ensure that
term of "x"'s type and term of "u"'s have the same subterm_spec.
Consequently,declaration.MRec argument has changed to the inductive name
instead of only the number of the inductive in the mutual_inductive
family.

In subterm_specif and check_rec_call, arguments are stored in a stack.
At each lambda, one element is popped to add in renv a smarter
subterm_spec for the variable. subterm_spec of constructor's argument
was added this way, the job is now done more often.

Some eta contracted match branches are now accepted but enforcing
eta-expansion of branches might be anyway a recommended invariant.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13012 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 7 deletions

diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index 3212b8eed..202b1aa4c 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -101,14 +101,11 @@ type guard_env =
   { env     : env;
     (** dB of last fixpoint *)
     rel_min : int;
-    (** inductive of recarg of each fixpoint *)
-    inds    : inductive array;
-    (** the recarg information of inductive family *)
-    recvec  : wf_paths array;
     (** dB of variables denoting subterms *)
     genv    : subterm_spec Lazy.t list;
   }
 
-val subterm_specif : guard_env -> constr -> subterm_spec
-val case_branches_specif : guard_env -> subterm_spec Lazy.t -> case_info ->
-  constr array -> (guard_env * constr) array
+type stack_element = |SClosure of guard_env*constr |SArg of subterm_spec Lazy.t
+
+val subterm_specif : guard_env -> stack_element list -> constr -> subterm_spec
+