diff options
Diffstat (limited to 'proofs/proof_global.ml')
| -rw-r--r-- | proofs/proof_global.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml index 6ffc79246..a3e240c8d 100644 --- a/proofs/proof_global.ml +++ b/proofs/proof_global.ml @@ -100,7 +100,7 @@ let _ = Errors.register_handler begin function | NoSuchProof -> Errors.error "No such proof." | _ -> raise Errors.Unhandled end -let rec extract id l = +let extract id l = let rec aux = function | ((id',_) as np)::l when id_ord id id' = 0 -> (np,l) | np::l -> let (np', l) = aux l in (np' , np::l) |