diff options
Diffstat (limited to 'contrib/extraction/extract_env.ml')
| -rw-r--r-- | contrib/extraction/extract_env.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index da5d0d9c1..9ca23646f 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -17,6 +17,7 @@ open Extraction open Miniml open Table open Mlutil +open Nametab open Vernacinterp open Common @@ -164,9 +165,9 @@ let _ = let c = Astterm.interp_constr Evd.empty (Global.env()) ast in match kind_of_term c with (* If it is a global reference, then output the declaration *) - | IsConst sp -> extract_reference (ConstRef sp) - | IsMutInd ind -> extract_reference (IndRef ind) - | IsMutConstruct cs -> extract_reference (ConstructRef cs) + | Const sp -> extract_reference (ConstRef sp) + | Ind ind -> extract_reference (IndRef ind) + | Construct cs -> extract_reference (ConstructRef cs) (* Otherwise, output the ML type or expression *) | _ -> match extract_constr (Global.env()) [] c with |