diff options
| author | Gaëtan Gilbert | 2019-05-28 17:25:32 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-05-28 17:25:32 +0200 |
| commit | be21788fc5cbe86af52d4f0ea21daa73ed8fcf4f (patch) | |
| tree | 69d6ac83951efa7d5006a8631a22403e380c1105 /dev | |
| parent | d4ca25df0f481345c99744acda28728c9682f0ac (diff) | |
Fix [Drop. #use "include";;] for indirect_accessor
Diffstat (limited to 'dev')
| -rw-r--r-- | dev/base_include | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/dev/base_include b/dev/base_include index b214959bad..f764eaf4f5 100644 --- a/dev/base_include +++ b/dev/base_include @@ -185,7 +185,7 @@ open Declareops;; let constbody_of_string s = let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_string s)) in - Option.get (Global.body_of_constant_body b);; + Option.get (Global.body_of_constant_body Library.indirect_accessor b);; (* Get the current goal *) (* |