diff options
Diffstat (limited to 'plugins/extraction/extraction.mli')
| -rw-r--r-- | plugins/extraction/extraction.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli index b15b88ed2..3a4ba0b34 100644 --- a/plugins/extraction/extraction.mli +++ b/plugins/extraction/extraction.mli @@ -9,9 +9,9 @@ (*s Extraction from Coq terms to Miniml. *) open Names -open Constr open Declarations open Environ +open Evd open Miniml val extract_constant : env -> Constant.t -> constant_body -> ml_decl @@ -20,16 +20,18 @@ val extract_constant_spec : env -> Constant.t -> constant_body -> ml_spec (** For extracting "module ... with ..." declaration *) -val extract_with_type : env -> constr -> ( Id.t list * ml_type ) option +val extract_with_type : + env -> evar_map -> EConstr.t -> ( Id.t list * ml_type ) option val extract_fixpoint : - env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl + env -> evar_map -> Constant.t array -> + (EConstr.t, EConstr.types) Constr.prec_declaration -> ml_decl val extract_inductive : env -> MutInd.t -> ml_ind (** For extraction compute *) -val extract_constr : env -> constr -> ml_ast * ml_type +val extract_constr : env -> evar_map -> EConstr.t -> ml_ast * ml_type (*s Is a [ml_decl] or a [ml_spec] logical ? *) |