From 06bd5357554ce06079b33288d3b9be0e68b44302 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 26 Jan 2010 16:51:00 +0000
Subject: Quick fix for references to section variables unbound in the current
 environment during unification. Should be checked earlier.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12692 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/unification.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping')

diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9156dfa9e2..d26195efc8 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -177,7 +177,7 @@ let use_evars_pattern_unification flags =
 
 let expand_key env = function
   | Some (ConstKey cst) -> constant_opt_value env cst
-  | Some (VarKey id) -> named_body id env
+  | Some (VarKey id) -> (try named_body id env with Not_found -> None)
   | Some (RelKey _) -> None
   | None -> None
 
-- 
cgit v1.2.3