diff options
| author | pboutill | 2010-05-18 15:57:18 +0000 |
|---|---|---|
| committer | pboutill | 2010-05-18 15:57:18 +0000 |
| commit | e7c9f5f130f5187e5d9b43c8f0ed15deb49e4b2c (patch) | |
| tree | 970e35349cfa40f40c51ba5089073210d450df51 /toplevel | |
| parent | 6cca4015db457f91b8eb9cf824f21246cbe7c6e6 (diff) | |
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
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/himsg.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml index 6c8847ff95..8fcf156084 100644 --- a/toplevel/himsg.ml +++ b/toplevel/himsg.ml @@ -227,7 +227,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = | RecursionNotOnInductiveType c -> str "Recursive definition on" ++ spc () ++ pr_lconstr_env env c ++ spc () ++ str "which should be an inductive type" - | RecursionOnIllegalTerm(j,arg,le,lt) -> + | RecursionOnIllegalTerm(j,(arg_env, arg),le,lt) -> let called = match names.(j) with Name id -> pr_id id @@ -245,7 +245,7 @@ let explain_ill_formed_rec_body env err names i fixenv vdefj = prlist_with_sep pr_spc pr_db lt in str "Recursive call to " ++ called ++ spc () ++ strbrk "has principal argument equal to" ++ spc () ++ - pr_lconstr_env env arg ++ strbrk " instead of " ++ vars + pr_lconstr_env arg_env arg ++ strbrk " instead of " ++ vars | NotEnoughArgumentsForFixCall j -> let called = |