diff options
| author | Pierre-Marie Pédrot | 2015-10-02 16:27:58 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-02 16:33:15 +0200 |
| commit | 944c8de0bfe4048e0733a487e6388db4dfc9075a (patch) | |
| tree | af037ad2d990da53529356fec44860ad9ca87577 /library/lib.ml | |
| parent | 16c88c9be5c37ee2e4fe04f7342365964031e7dd (diff) | |
| parent | 8860362de4a26286b0cb20cf4e02edc5209bdbd1 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'library/lib.ml')
| -rw-r--r-- | library/lib.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/library/lib.ml b/library/lib.ml index 81db547efd..f4f52db53b 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -420,6 +420,7 @@ let extract_hyps (secs,ohyps) = in aux (secs,ohyps) let instance_from_variable_context sign = + let rec inst_rec = function | (id,b,None,_) :: sign -> id :: inst_rec sign | _ :: sign -> inst_rec sign |