diff options
| -rw-r--r-- | library/heads.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/library/heads.ml b/library/heads.ml index 3f7c8877e..8fda452c1 100644 --- a/library/heads.ml +++ b/library/heads.ml @@ -66,12 +66,8 @@ let _ = Summary.unfreeze_function = unfreeze; Summary.init_function = init } -let variable_head id = - try Evalrefmap.find (EvalVarRef id) !head_map - with Not_found -> assert false -let constant_head cst = - try Evalrefmap.find (EvalConstRef cst) !head_map - with Not_found -> assert false +let variable_head id = Evalrefmap.find (EvalVarRef id) !head_map +let constant_head cst = Evalrefmap.find (EvalConstRef cst) !head_map let kind_of_head env t = let rec aux k l t b = match kind_of_term (Reduction.whd_betaiotazeta t) with |