diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-12 23:34:49 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-12 23:34:49 +0000 |
| commit | b57991c34dfc88820eee14e2962aa0833cbc3fe9 (patch) | |
| tree | 800bbdf7339d7f17e915999cd84616d61b87fa77 | |
| parent | ce7054e5eb47c5bf2bc569ef7af1b90fa7a00bca (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.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 |