diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-05-28 14:13:12 +0200 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2015-05-28 14:13:12 +0200 |
| commit | 83188dacc43df02245d13810d08cc63b7a5633ed (patch) | |
| tree | 52ee188c2f638dc9a27a480977f00a521f6a5dff /pretyping/evd.ml | |
| parent | 5c437ab917bd24de66986e95dcf58c3f31e17a34 (diff) | |
Fixup for 866c41b
Diffstat (limited to 'pretyping/evd.ml')
| -rw-r--r-- | pretyping/evd.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evd.ml b/pretyping/evd.ml index fe96aa347..60b1da704 100644 --- a/pretyping/evd.ml +++ b/pretyping/evd.ml @@ -339,7 +339,7 @@ let evar_universe_context_set diff ctx = match Univ.LMap.find l ctx.uctx_univ_variables with | Some u -> Univ.Constraint.add (l, Univ.Eq, Option.get (Univ.Universe.level u)) cstrs | None -> cstrs - with Not_found -> cstrs) + with Not_found | Option.IsNone -> cstrs) (Univ.Instance.levels (Univ.UContext.instance diff)) Univ.Constraint.empty in Univ.ContextSet.add_constraints cstrs initctx |