From e7c9f5f130f5187e5d9b43c8f0ed15deb49e4b2c Mon Sep 17 00:00:00 2001 From: pboutill Date: Tue, 18 May 2010 15:57:18 +0000 Subject: 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 --- plugins/decl_mode/decl_proof_instr.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins') diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index 97a56cabe..aadd04547 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -806,7 +806,7 @@ let is_rec_pos (main_ind,wft) = None -> false | Some index -> match fst (Rtree.dest_node wft) with - Mrec i when i = index -> true + Mrec (_,i) when i = index -> true | _ -> false let rec constr_trees (main_ind,wft) ind = -- cgit v1.2.3