diff options
| author | msozeau | 2008-09-11 18:28:41 +0000 |
|---|---|---|
| committer | msozeau | 2008-09-11 18:28:41 +0000 |
| commit | 5953161cd65194e341b2f8255501e7a15de498ac (patch) | |
| tree | 6e3baa7b3ac9f85d82399dc4fb62f121b3f695ec /contrib/funind | |
| parent | cb18488b07fb6f9ba3e6e7ac854bbe68aa630e39 (diff) | |
Add enough information to correctly globalize recursive calls in inductive and
recursive definitions and references to previous fields in record and
classes definitions. Fixes the corresponding typesetting issue in coqdoc
output.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11397 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind')
| -rw-r--r-- | contrib/funind/indfun.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 79ef009729..027aae7a79 100644 --- a/contrib/funind/indfun.ml +++ b/contrib/funind/indfun.ml @@ -168,7 +168,7 @@ let build_newrecursive if Impargs.is_implicit_args() then Impargs.compute_implicits env0 arity else [] in - let impls' =(recname,([],impl,Notation.compute_arguments_scope arity))::impls in + let impls' =(recname,(Constrintern.Recursive,[],impl,Notation.compute_arguments_scope arity))::impls in (Environ.push_named (recname,None,arity) env, impls')) (env0,[]) lnameargsardef in let recdef = |