From b6feaafc7602917a8ef86fb8adc9651ff765e710 Mon Sep 17 00:00:00 2001
From: Matej Košík
Date: Mon, 29 May 2017 11:02:06 +0200
Subject: Remove (useless) aliases from the API.

---
 plugins/extraction/extraction.mli | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/extraction/extraction.mli')

diff --git a/plugins/extraction/extraction.mli b/plugins/extraction/extraction.mli
index 2b4b05a957..26268fb177 100644
--- a/plugins/extraction/extraction.mli
+++ b/plugins/extraction/extraction.mli
@@ -15,18 +15,18 @@ open Declarations
 open Environ
 open Miniml
 
-val extract_constant : env -> constant -> constant_body -> ml_decl
+val extract_constant : env -> Constant.t -> constant_body -> ml_decl
 
-val extract_constant_spec : env -> constant -> constant_body -> ml_spec
+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_fixpoint :
-  env -> constant array -> (constr, types) prec_declaration -> ml_decl
+  env -> Constant.t array -> (constr, types) prec_declaration -> ml_decl
 
-val extract_inductive : env -> mutual_inductive -> ml_ind
+val extract_inductive : env -> MutInd.t -> ml_ind
 
 (** For extraction compute *)
 
-- 
cgit v1.2.3