diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-01-17 14:23:53 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2017-04-24 23:58:23 +0200 |
| commit | 158f40db9482ead89befbf9bc9ad45ff8a60b75f (patch) | |
| tree | 92587db07ddf50e2db16b270966115fa3d66d64a /plugins/funind/indfun_common.ml | |
| parent | be83b52cf50ed4c596e40cfd52da03258a7a4a18 (diff) | |
[location] Switch glob_constr to Loc.located
Diffstat (limited to 'plugins/funind/indfun_common.ml')
| -rw-r--r-- | plugins/funind/indfun_common.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml index 7b0d7d27d..8f0c98624 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -69,9 +69,9 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt 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 + match Loc.obj rt 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 | _ -> raise (CErrors.UserError(Some "chop_rlambda_n", str "chop_rlambda_n: Not enough Lambdas")) @@ -83,8 +83,8 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt with - | Glob_term.GProd(_,name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b + match Loc.obj rt 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 chop_prod_n [] |