aboutsummaryrefslogtreecommitdiff
path: root/interp/constrintern.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r--interp/constrintern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 5151d2a10a..8f0d56c5bd 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1913,7 +1913,7 @@ let interp_rawcontext_evars env evdref bl =
| Some b ->
let c = understand_judgment_tcc env evdref b in
let d = (na, Some c.uj_val, c.uj_type) in
- (push_rel d env, d::params, succ n, impls))
+ (push_rel d env, d::params, n, impls))
(env,[],1,[]) (List.rev bl)
in (env, par), impls