diff options
author | 2001-04-19 14:55:01 +0000 | |
---|---|---|
committer | 2001-04-19 14:55:01 +0000 | |
commit | fe45801c1fdfebeacaf5daa0569d89838b11774f (patch) | |
tree | 89ae2aeb40002953befb5679f2c2bb618515b023 /contrib/extraction/extract_env.ml | |
parent | b86ca8cf94dfc0b7127725ec31f7c33adba67cad (diff) |
cofix; axiomes; eta-expansions pour variables de types mal generalisees (en cours)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1633 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction/extract_env.ml')
-rw-r--r-- | contrib/extraction/extract_env.ml | 18 |
1 files changed, 11 insertions, 7 deletions
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml index 616591048..c99d270ca 100644 --- a/contrib/extraction/extract_env.ml +++ b/contrib/extraction/extract_env.ml @@ -110,6 +110,13 @@ module Pp = Ocaml.Make(ToplevelParams) open Vernacinterp +let extract_reference r = + mSGNL + (if is_ml_extraction r then + [< 'sTR "User defined extraction:"; 'sPC; 'sTR (find_ml_extraction r) >] + else + Pp.pp_decl (extract_declaration r)) + let _ = vinterp_add "Extraction" (function @@ -118,12 +125,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,_) -> - mSGNL (Pp.pp_decl (extract_declaration (ConstRef sp))) - | IsMutInd (ind,_) -> - mSGNL (Pp.pp_decl (extract_declaration (IndRef ind))) - | IsMutConstruct (cs,_) -> - mSGNL (Pp.pp_decl (extract_declaration (ConstructRef cs))) + | IsConst (sp,_) -> extract_reference (ConstRef sp) + | IsMutInd (ind,_) -> extract_reference (IndRef ind) + | IsMutConstruct (cs,_) -> extract_reference (ConstructRef cs) (* Otherwise, output the ML type or expression *) | _ -> match extract_constr (Global.env()) [] c with @@ -196,7 +200,7 @@ let extract_module m = let get_reference = function | sp, Leaf o -> (match Libobject.object_tag o with - | "CONSTANT" -> ConstRef sp + | "CONSTANT" | "PARAMETER" -> ConstRef sp | "INDUCTIVE" -> IndRef (sp,0) | _ -> failwith "caught") | _ -> failwith "caught" |