diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-24 17:35:05 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-10-24 17:42:14 +0200 |
| commit | 1556c6b8f77d16814ff1c53fb14fc9b06574ec4b (patch) | |
| tree | 7c3085729fea24ebf5b12d785da22e528e38174a /kernel/context.ml | |
| parent | 08e87eb96ab67ead60d92394eec6066d9b52e55e (diff) | |
Remove an ununsed pattern and commented code in the kernel.
Reestablish completeness in conversion when Opaque primitive
projections are used.
Diffstat (limited to 'kernel/context.ml')
| -rw-r--r-- | kernel/context.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/context.ml b/kernel/context.ml index 6b5a6cdb9..e43e08865 100644 --- a/kernel/context.ml +++ b/kernel/context.ml @@ -80,7 +80,7 @@ let rel_context_tags ctx = let rec aux l = function | [] -> l | (_,Some _,_)::ctx -> aux (true::l) ctx - | (_,None _,_)::ctx -> aux (false::l) ctx + | (_,None,_)::ctx -> aux (false::l) ctx in aux [] ctx (*s Signatures of named hypotheses. Used for section variables and |