From b35582012e9f7923ca2e55bfbfae9215770f8fbd Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Sun, 25 Nov 2012 17:39:07 +0000
Subject: Monomorphization (library)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16001 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/decls.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library/decls.ml')

diff --git a/library/decls.ml b/library/decls.ml
index f6fa626b17..af6ee34484 100644
--- a/library/decls.ml
+++ b/library/decls.ml
@@ -9,6 +9,7 @@
 (** This module registers tables for some non-logical informations
      associated declarations *)
 
+open Util
 open Names
 open Sign
 open Decl_kinds
@@ -64,7 +65,7 @@ let initialize_named_context_for_proof () =
 let last_section_hyps dir =
   fold_named_context
     (fun (id,_,_) sec_ids ->
-      try if dir=variable_path id then id::sec_ids else sec_ids
+      try if dir_path_eq dir (variable_path id) then id::sec_ids else sec_ids
       with Not_found -> sec_ids)
     (Environ.named_context (Global.env()))
     ~init:[]
-- 
cgit v1.2.3