diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:43 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:43 +0100 |
| commit | 9c775561f67ac558c2c408cfa873544e2fea7b0a (patch) | |
| tree | 375ac16822f815477b36d50e49bb3cd9633aaa84 /contrib/funind/indfun.ml | |
| parent | 3e6a1167fd397f2c72b48315e5d82f6c7e24703f (diff) | |
| parent | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (diff) | |
Merge commit 'upstream/8.2.rc2+dfsg'
Diffstat (limited to 'contrib/funind/indfun.ml')
| -rw-r--r-- | contrib/funind/indfun.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/funind/indfun.ml b/contrib/funind/indfun.ml index 79ef0097..b6b2cbd1 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 = @@ -612,7 +612,9 @@ let rec add_args id new_args b = CCast(loc,add_args id new_args b1,CastConv(ck,add_args id new_args b2)) | CCast(loc,b1,CastCoerce) -> CCast(loc,add_args id new_args b1,CastCoerce) + | CRecord _ -> anomaly "add_args : CRecord" | CNotation _ -> anomaly "add_args : CNotation" + | CGeneralization _ -> anomaly "add_args : CGeneralization" | CPrim _ -> b | CDelimiters _ -> anomaly "add_args : CDelimiters" | CDynamic _ -> anomaly "add_args : CDynamic" |