aboutsummaryrefslogtreecommitdiff
path: root/pretyping/evarutil.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/evarutil.ml')
-rw-r--r--pretyping/evarutil.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 38edd1e320..87fd809630 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -220,7 +220,7 @@ let new_isevar isevars env typ k =
let (sigma',evar) =
new_isevar_sign env' !isevars typ' (Array.of_list newargs) in
isevars := sigma';
- (evar,typ')
+ evar