diff options
Diffstat (limited to 'contrib/subtac')
| -rw-r--r-- | contrib/subtac/infer.ml | 2 | ||||
| -rw-r--r-- | contrib/subtac/rewrite.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/subtac/infer.ml b/contrib/subtac/infer.ml index 876dc68bb..987fbedda 100644 --- a/contrib/subtac/infer.ml +++ b/contrib/subtac/infer.ml @@ -6,7 +6,7 @@ open Util open Sast open Scoq open Pp -open Ppconstrnew +open Ppconstr let ($) f g = fun x -> f (g x) diff --git a/contrib/subtac/rewrite.ml b/contrib/subtac/rewrite.ml index ce0f15ec2..b228be2a7 100644 --- a/contrib/subtac/rewrite.ml +++ b/contrib/subtac/rewrite.ml @@ -7,7 +7,7 @@ open Term open Names open Scoq open Pp -open Ppconstrnew +open Ppconstr open Util type recursion_info = { |