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/ltac/pptactic.ml | |
| parent | 276f08cb053eed175478c4c9359e61fb949742ba (diff) | |
| parent | 1db568d3dc88d538f975377bb4d8d3eecd87872c (diff) | |
Merge PR #914: Making the detyper lazy
Diffstat (limited to 'plugins/ltac/pptactic.ml')
| -rw-r--r-- | plugins/ltac/pptactic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml index cb7d9b9c02..f4e3ba633f 100644 --- a/plugins/ltac/pptactic.ml +++ b/plugins/ltac/pptactic.ml @@ -1040,7 +1040,7 @@ type 'a extra_genarg_printer = let strip_prod_binders_glob_constr n (ty,_) = let rec strip_ty acc n ty = if Int.equal n 0 then (List.rev acc, (ty,None)) else - match ty.CAst.v with + match DAst.get ty with Glob_term.GProd(na,Explicit,a,b) -> strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in |