diff options
| author | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-09-07 12:44:47 +0200 |
| commit | 084ef41c98d52078f85831c940d0a073a4ccdb7a (patch) | |
| tree | f1808d72e562f0dd674759f2f447f44cd5da9aad /plugins/funind/indfun_common.ml | |
| parent | 276f08cb053eed175478c4c9359e61fb949742ba (diff) | |
| parent | 1db568d3dc88d538f975377bb4d8d3eecd87872c (diff) | |
Merge PR #914: Making the detyper lazy
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 f4f9ba2bbb..5f4d514f36 100644 --- a/plugins/funind/indfun_common.ml +++ b/plugins/funind/indfun_common.ml @@ -66,7 +66,7 @@ let chop_rlambda_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get 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 | _ -> @@ -80,7 +80,7 @@ let chop_rprod_n = if n == 0 then List.rev acc,rt else - match rt.CAst.v with + match DAst.get 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 |