aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evd.ml7
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 8243f96c16..842b87c57e 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1136,9 +1136,10 @@ let make_evar_universe_context e l =
match l with
| None -> uctx
| Some us ->
- List.fold_left (fun uctx (loc,id) ->
- fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) uctx))
- uctx us
+ List.fold_left
+ (fun uctx (loc,id) ->
+ fst (uctx_new_univ_variable univ_rigid (Some (Id.to_string id)) true uctx))
+ uctx us
(****************************************)
(* Operations on constants *)