aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-12 23:34:49 +0000
committerGravatar letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>2011-10-12 23:34:49 +0000
commitb57991c34dfc88820eee14e2962aa0833cbc3fe9 (patch)
tree800bbdf7339d7f17e915999cd84616d61b87fa77
parentce7054e5eb47c5bf2bc569ef7af1b90fa7a00bca (diff)
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
-rw-r--r--library/heads.ml8
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