diff options
| author | Emilio Jesus Gallego Arias | 2017-04-09 03:35:20 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2017-04-25 00:33:36 +0200 |
| commit | ee2197096fe75a63b4d92cb3a1bb05122c5c625b (patch) | |
| tree | 3b40c06375a463625a2675b90e009fcb0b64a7d2 /plugins/funind/indfun_common.ml | |
| parent | 054d2736c1c1b55cb7708ff0444af521cd0fe2ba (diff) | |
[location] [ast] Port module AST to CAst
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index de8dc53f11..394b252aac 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -69,7 +69,7 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match Loc.obj rt with + match rt.CAst.v with | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b | _ -> @@ -83,7 +83,7 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match Loc.obj rt with + match rt.CAst.v with | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products")) in |