From b57991c34dfc88820eee14e2962aa0833cbc3fe9 Mon Sep 17 00:00:00 2001 From: letouzey Date: Wed, 12 Oct 2011 23:34:49 +0000 Subject: Temporary revert commit 14550 since it breaks a few contribs Interestingly, it appears that the Not_found in heads.ml is actually triggered in some contribs, but catched. Maybe a "try" tactical ? Are these Not_found another effects of bug #2608 or something similar ? Anyway, replacing Not_found by "assert false" currently breaks these contribs. So for the moment, we revert to the original code. When bug #2608 will have been solved, we'll try again enabling these "assert false". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14560 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/heads.ml | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) (limited to 'library/heads.ml') 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 -- cgit v1.2.3