From e0da5c0227680becfc9bf87046b26afb290c55a3 Mon Sep 17 00:00:00 2001
From: msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 23 Feb 2012 14:38:57 +0000
Subject: Implement the substitution function for global options. Fixes anomaly
 in ssreflect compilation

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

(limited to 'library/goptions.ml')

diff --git a/library/goptions.ml b/library/goptions.ml
index 90c8728c1..5af186899 100644
--- a/library/goptions.ml
+++ b/library/goptions.ml
@@ -247,6 +247,7 @@ let declare_option cast uncast
       declare_object {(default_object ("G  "^nickname key)) with
 		       cache_function = (fun (_,v) -> write v);
 		       classify_function = (fun v -> Substitute v);
+		       subst_function = (fun (_,v) -> v);
 		       discharge_function = (fun (_,v) -> Some v);
 		       load_function = (fun _ (_,v) -> write v)}
     in
-- 
cgit v1.2.3