aboutsummaryrefslogtreecommitdiffstats
path: root/cfrontend/SimplExpr.v
diff options
context:
space:
mode:
Diffstat (limited to 'cfrontend/SimplExpr.v')
-rw-r--r--cfrontend/SimplExpr.v2
1 files changed, 1 insertions, 1 deletions
diff --git a/cfrontend/SimplExpr.v b/cfrontend/SimplExpr.v
index 0a191f29..45b686f3 100644
--- a/cfrontend/SimplExpr.v
+++ b/cfrontend/SimplExpr.v
@@ -80,7 +80,7 @@ Definition initial_generator (x: unit) : generator :=
Definition gensym (ty: type): mon ident :=
fun (g: generator) =>
Res (gen_next g)
- (mkgenerator (Psucc (gen_next g)) ((gen_next g, ty) :: gen_trail g))
+ (mkgenerator (Pos.succ (gen_next g)) ((gen_next g, ty) :: gen_trail g))
(Ple_succ (gen_next g)).
(** Construct a sequence from a list of statements. To facilitate the