aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/FunInd.v2
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/functional_principles_proofs.ml10
-rw-r--r--plugins/funind/functional_principles_proofs.mli5
-rw-r--r--plugins/funind/functional_principles_types.ml5
-rw-r--r--plugins/funind/functional_principles_types.mli5
-rw-r--r--plugins/funind/g_indfun.ml44
-rw-r--r--plugins/funind/glob_term_to_relation.ml9
-rw-r--r--plugins/funind/glob_term_to_relation.mli1
-rw-r--r--plugins/funind/glob_termops.ml1
-rw-r--r--plugins/funind/glob_termops.mli1
-rw-r--r--plugins/funind/indfun.ml85
-rw-r--r--plugins/funind/indfun.mli3
-rw-r--r--plugins/funind/indfun_common.ml3
-rw-r--r--plugins/funind/indfun_common.mli5
-rw-r--r--plugins/funind/invfun.ml13
-rw-r--r--plugins/funind/merge.ml5
-rw-r--r--plugins/funind/recdef.ml7
-rw-r--r--plugins/funind/recdef.mli5
19 files changed, 74 insertions, 97 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
index e40aea7764..b8a05e5cc0 100644
--- a/plugins/funind/FunInd.v
+++ b/plugins/funind/FunInd.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index 64f43b8335..8b4dbbb45c 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ef894b2395..15ab396e31 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1,4 +1,3 @@
-open API
open Printer
open CErrors
open Util
@@ -10,7 +9,6 @@ open Names
open Pp
open Tacmach
open Termops
-open Proof_type
open Tacticals
open Tactics
open Indfun_common
@@ -106,7 +104,7 @@ let make_refl_eq constructor type_of_t t =
type pte_info =
{
- proving_tac : (Id.t list -> Proof_type.tactic);
+ proving_tac : (Id.t list -> Tacmach.tactic);
is_valid : constr -> bool
}
@@ -958,7 +956,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (fst (destConst evd f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let f_body = Option.get (Global.body_of_constant_body f_def) in
+ let (f_body, _) = Option.get (Global.body_of_constant_body f_def) in
let f_body = EConstr.of_constr f_body in
let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1092,7 +1090,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let get_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
@@ -1383,7 +1381,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(* Proof of principles of general functions *)
-(* let hrec_id =
+(* let hrec_id = Recdef.hrec_id *)
(* and acc_inv_id = Recdef.acc_inv_id *)
(* and ltof_ref = Recdef.ltof_ref *)
(* and acc_rel = Recdef.acc_rel *)
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 5bb288678d..64fbfaeedf 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -1,10 +1,9 @@
-open API
open Names
val prove_princ_for_struct :
Evd.evar_map ref ->
bool ->
- int -> Constant.t array -> EConstr.constr array -> int -> Proof_type.tactic
+ int -> Constant.t array -> EConstr.constr array -> int -> Tacmach.tactic
val prove_principle_for_gen :
@@ -14,7 +13,7 @@ val prove_principle_for_gen :
int -> (* the number of recursive argument *)
EConstr.types -> (* the type of the recursive argument *)
EConstr.constr -> (* the wf relation used to prove the function *)
- Proof_type.tactic
+ Tacmach.tactic
(* val is_pte : rel_declaration -> bool *)
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8ffd15f9fb..513fce2484 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -1,4 +1,3 @@
-open API
open Printer
open CErrors
open Util
@@ -407,7 +406,7 @@ let get_funs_constant mp dp =
function const ->
let find_constant_body const =
match Global.body_of_constant const with
- | Some body ->
+ | Some (body, _) ->
let body = Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
@@ -651,7 +650,7 @@ let build_case_scheme fa =
(* in *)
let funs =
let (_,f,_) = fa in
- try fst (Universes.unsafe_constr_of_global (Smartlocate.global_with_alias f))
+ try fst (Global.constr_of_global_in_context (Global.env ()) (Smartlocate.global_with_alias f))
with Not_found ->
user_err ~hdr:"FunInd.build_case_scheme"
(str "Cannot find " ++ Libnames.pr_reference f) in
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index bb2b2d9186..5a7ffe0590 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Names
open Term
open Misctypes
@@ -28,7 +27,7 @@ val generate_functional_principle :
(* The tactic to use to make the proof w.r
the number of params
*)
- (EConstr.constr array -> int -> Proof_type.tactic) ->
+ (EConstr.constr array -> int -> Tacmach.tactic) ->
unit
val compute_new_princ_type_from_rel : constr array -> Sorts.t array ->
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 1258c92868..16d9f200f3 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
(*i camlp4deps: "grammar/grammar.cma" i*)
-open API
-open Grammar_API
open Ltac_plugin
open Util
open Pp
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0e2ca49000..379c83b245 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1,4 +1,3 @@
-open API
open Printer
open Pp
open Names
@@ -1459,7 +1458,9 @@ let do_build_inductive
(* in *)
let _time2 = System.get_time () in
try
- with_full_print (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false)) Decl_kinds.Finite
+ with_full_print
+ (Flags.silently (Command.do_mutual_inductive rel_inds (Flags.is_universe_polymorphism ()) false false))
+ Decl_kinds.Finite
with
| UserError(s,msg) as e ->
let _time3 = System.get_time () in
@@ -1470,7 +1471,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
++ fnl () ++
msg
in
@@ -1485,7 +1486,7 @@ let do_build_inductive
in
let msg =
str "while trying to define"++ spc () ++
- Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,Decl_kinds.Finite,repacked_rel_inds))
+ Ppvernac.pr_vernac (Vernacexpr.VernacInductive(false,false,Decl_kinds.Finite,repacked_rel_inds))
++ fnl () ++
CErrors.print reraise
in
diff --git a/plugins/funind/glob_term_to_relation.mli b/plugins/funind/glob_term_to_relation.mli
index 7ad7de0792..0cab5a6d35 100644
--- a/plugins/funind/glob_term_to_relation.mli
+++ b/plugins/funind/glob_term_to_relation.mli
@@ -1,4 +1,3 @@
-open API
open Names
(*
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 726a8203d7..7cb35838c7 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -1,4 +1,3 @@
-open API
open Pp
open Glob_term
open CErrors
diff --git a/plugins/funind/glob_termops.mli b/plugins/funind/glob_termops.mli
index b6d2c45437..99a258de98 100644
--- a/plugins/funind/glob_termops.mli
+++ b/plugins/funind/glob_termops.mli
@@ -1,4 +1,3 @@
-open API
open Names
open Glob_term
open Misctypes
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d12aa7f425..863c9dc8d5 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -1,4 +1,3 @@
-open API
open CErrors
open Util
open Names
@@ -343,7 +342,7 @@ let error_error names e =
let generate_principle (evd:Evd.evar_map ref) pconstants on_error
is_general do_built (fix_rec_l:(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) recdefs interactive_proof
(continue_proof : int -> Names.Constant.t array -> EConstr.constr array -> int ->
- Proof_type.tactic) : unit =
+ Tacmach.tactic) : unit =
let names = List.map (function (((_, name),_),_,_,_,_),_ -> name) fix_rec_l in
let fun_bodies = List.map2 prepare_body fix_rec_l recdefs in
let funs_args = List.map fst fun_bodies in
@@ -446,7 +445,7 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
let generate_correction_proof_wf f_ref tcc_lemma_ref
is_mes functional_ref eq_ref rec_arg_num rec_arg_type nb_args relation
- (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Proof_type.tactic =
+ (_: int) (_:Names.Constant.t array) (_:EConstr.constr array) (_:int) : Tacmach.tactic =
Functional_principles_proofs.prove_principle_for_gen
(f_ref,functional_ref,eq_ref)
tcc_lemma_ref is_mes rec_arg_num rec_arg_type relation
@@ -576,50 +575,44 @@ let map_option f = function
| Some v -> Some (f v)
open Constrexpr
-open Topconstr
-let make_assoc assoc l1 l2 =
- let fold assoc a b = match a, b with
- | (_, Name na), (_, Name id) -> Id.Map.add na id assoc
- | _, _ -> assoc
- in
- List.fold_left2 fold assoc l1 l2
-
-let rec rebuild_bl (aux,assoc) bl typ =
- match bl,typ with
- | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
- | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
- rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
- | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } ->
- rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
+let rec rebuild_bl aux bl typ =
+ match bl,typ with
+ | [], _ -> List.rev aux,typ
+ | (CLocalAssum(nal,bk,_))::bl',typ ->
+ rebuild_nal aux bk bl' nal typ
+ | (CLocalDef(na,_,_))::bl',{ CAst.v = CLetIn(_,nat,ty,typ') } ->
+ rebuild_bl (Constrexpr.CLocalDef(na,nat,ty)::aux)
bl' typ'
| _ -> assert false
- and rebuild_nal (aux,assoc) bk bl' nal lnal typ =
- match nal, typ.CAst.v with
- | [], _ -> rebuild_bl (aux,assoc) bl' typ
- | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
- | _,CProdN((nal',bk',nal't)::rest,typ') ->
- let lnal' = List.length nal' in
- if lnal' >= lnal
- then
- let old_nal',new_nal' = List.chop lnal nal' in
- let nassoc = make_assoc assoc old_nal' nal in
- let assum = CLocalAssum(nal,bk,replace_vars_constr_expr assoc nal't) in
- rebuild_bl ((assum :: aux), nassoc) bl'
- (if List.is_empty new_nal' && List.is_empty rest
- then typ'
- else CAst.make @@ if List.is_empty new_nal'
- then CProdN(rest,typ')
- else CProdN(((new_nal',bk',nal't)::rest),typ'))
- else
- let captured_nal,non_captured_nal = List.chop lnal' nal in
- let nassoc = make_assoc assoc nal' captured_nal in
- let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
- rebuild_nal ((assum :: aux), nassoc)
- bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ'))
- | _ -> assert false
-
-let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
+and rebuild_nal aux bk bl' nal typ =
+ match nal,typ with
+ | _,{ CAst.v = CProdN([],typ) } -> rebuild_nal aux bk bl' nal typ
+ | [], _ -> rebuild_bl aux bl' typ
+ | na::nal,{ CAst.v = CProdN((na'::nal',bk',nal't)::rest,typ') } ->
+ if Name.equal (snd na) (snd na') || Name.is_anonymous (snd na')
+ then
+ let assum = CLocalAssum([na],bk,nal't) in
+ let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ rebuild_nal
+ (assum::aux)
+ bk
+ bl'
+ nal
+ (CAst.make @@ CProdN(new_rest,typ'))
+ else
+ let assum = CLocalAssum([na'],bk,nal't) in
+ let new_rest = if nal' = [] then rest else ((nal',bk',nal't)::rest) in
+ rebuild_nal
+ (assum::aux)
+ bk
+ bl'
+ (na::nal)
+ (CAst.make @@ CProdN(new_rest,typ'))
+ | _ ->
+ assert false
+
+let rebuild_bl aux bl typ = rebuild_bl aux bl typ
let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) list) =
let fixl,ntns = Command.extract_fixpoint_components false fixpoint_exprl in
@@ -629,7 +622,7 @@ let recompute_binder_list (fixpoint_exprl : (Vernacexpr.fixpoint_expr * Vernacex
let fixpoint_exprl_with_new_bl =
List.map2 (fun ((lna,(rec_arg_opt,rec_order),bl,ret_typ,opt_body),notation_list) fix_typ ->
- let new_bl',new_ret_type,_ = rebuild_bl ([],Id.Map.empty) bl fix_typ in
+ let new_bl',new_ret_type = rebuild_bl [] bl fix_typ in
(((lna,(rec_arg_opt,rec_order),new_bl',new_ret_type,opt_body),notation_list):(Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list))
)
fixpoint_exprl constr_expr_typel
@@ -857,7 +850,7 @@ let make_graph (f_ref:global_reference) =
in
(match Global.body_of_constant_body c_body with
| None -> error "Cannot build a graph over an axiom!"
- | Some body ->
+ | Some (body, _) ->
let env = Global.env () in
let sigma = Evd.from_env env in
let extern_body,extern_type =
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 33420d8132..7a60da44fb 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -1,4 +1,3 @@
-open API
open Misctypes
val warn_cannot_define_graph : ?loc:Loc.t -> Pp.std_ppcmds * Pp.std_ppcmds -> unit
@@ -16,7 +15,7 @@ val functional_induction :
EConstr.constr ->
(EConstr.constr * EConstr.constr bindings) option ->
Tacexpr.or_and_intro_pattern option ->
- Proof_type.goal Evd.sigma -> Proof_type.goal list Evd.sigma
+ Goal.goal Evd.sigma -> Goal.goal list Evd.sigma
val make_graph : Globnames.global_reference -> unit
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 6fe6888f3d..f4f9ba2bbb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -1,4 +1,3 @@
-open API
open Names
open Pp
open Libnames
@@ -342,7 +341,7 @@ let pr_info f_info =
str "function_constant_type := " ++
(try
Printer.pr_lconstr
- (Global.type_of_global_unsafe (ConstRef f_info.function_constant))
+ (fst (Global.type_of_global_in_context (Global.env ()) (ConstRef f_info.function_constant)))
with e when CErrors.noncritical e -> mt ()) ++ fnl () ++
str "equation_lemma := " ++ pr_ocst f_info.equation_lemma ++ fnl () ++
str "completeness_lemma :=" ++ pr_ocst f_info.completeness_lemma ++ fnl () ++
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6b40c91713..5e425cd18a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,4 +1,3 @@
-open API
open Names
open Pp
@@ -105,7 +104,7 @@ exception ToShow of exn
val is_strict_tcc : unit -> bool
-val h_intros: Names.Id.t list -> Proof_type.tactic
+val h_intros: Names.Id.t list -> Tacmach.tactic
val h_id : Names.Id.t
val hrec_id : Names.Id.t
val acc_inv_id : EConstr.constr Util.delayed
@@ -114,7 +113,7 @@ val well_founded_ltof : EConstr.constr Util.delayed
val acc_rel : EConstr.constr Util.delayed
val well_founded : EConstr.constr Util.delayed
val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
-val list_rewrite : bool -> (EConstr.constr*bool) list -> Proof_type.tactic
+val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
(Names.Name.t * EConstr.t) list * EConstr.t
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ebdb490e37..8dea6c90f5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
open Ltac_plugin
open Declarations
open CErrors
@@ -218,7 +217,7 @@ let rec generate_fresh_id x avoid i =
\end{enumerate}
*)
-let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Proof_type.tactic =
+let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes lemmas_types_infos i : Tacmach.tactic =
fun g ->
(* first of all we recreate the lemmas types to be used as predicates of the induction principle
that is~:
@@ -468,7 +467,7 @@ let tauto =
let rec intros_with_rewrite g =
observe_tac "intros_with_rewrite" intros_with_rewrite_aux g
-and intros_with_rewrite_aux : Proof_type.tactic =
+and intros_with_rewrite_aux : Tacmach.tactic =
fun g ->
let eq_ind = make_eq () in
let sigma = project g in
@@ -629,7 +628,7 @@ let rec reflexivity_with_destruct_cases g =
*)
-let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.tactic =
+let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Tacmach.tactic =
fun g ->
(* We compute the types of the different mutually recursive lemmas
in $\zeta$ normal form
@@ -673,7 +672,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : Proof_type.ta
using [f_equation] if it is recursive (that is the graph is infinite
or unfold if the graph is finite
*)
- let rewrite_tac j ids : Proof_type.tactic =
+ let rewrite_tac j ids : Tacmach.tactic =
let graph_def = graphs.(j) in
let infos =
try find_Function_infos (fst (destConst (project g) funcs.(j)))
@@ -953,7 +952,7 @@ let revert_graph kn post_tac hid g =
\end{enumerate}
*)
-let functional_inversion kn hid fconst f_correct : Proof_type.tactic =
+let functional_inversion kn hid fconst f_correct : Tacmach.tactic =
fun g ->
let old_ids = List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty in
let sigma = project g in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index c75f7f868c..52a82b0e5e 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,6 @@
(* Merging of induction principles. *)
-open API
open Globnames
open Tactics
open Indfun_common
@@ -880,7 +879,7 @@ let merge_inductive (ind1: inductive) (ind2: inductive)
(* Declare inductive *)
let indl,_,_ = Command.extract_mutual_inductive_declaration_components [(indexpr,[])] in
let mie,pl,impls = Command.interp_mutual_inductive indl []
- false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
+ false (* non-cumulative *) false (*FIXMEnon-poly *) false (* means not private *) Decl_kinds.Finite (* means: not coinductive *) in
(* Declare the mutual inductive block with its associated schemes *)
ignore (Command.declare_mutual_inductive_with_eliminations mie pl impls)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3cd20a9507..d3eccb58d7 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,12 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open API
module CVars = Vars
@@ -30,7 +29,7 @@ open Nametab
open Declare
open Decl_kinds
open Tacred
-open Proof_type
+open Goal
open Pfedit
open Glob_term
open Pretyping
@@ -90,7 +89,7 @@ let type_of_const sigma t =
|_ -> assert false
let constr_of_global x =
- fst (Universes.unsafe_constr_of_global x)
+ fst (Global.constr_of_global_in_context (Global.env ()) x)
let constant sl s = constr_of_global (find_reference sl s)
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index e1a072799e..63bbdbe7e3 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -1,11 +1,10 @@
-open API
(* val evaluable_of_global_reference : Libnames.global_reference -> Names.evaluable_global_reference *)
val tclUSER_if_not_mes :
- Proof_type.tactic ->
+ Tacmach.tactic ->
bool ->
Names.Id.t list option ->
- Proof_type.tactic
+ Tacmach.tactic
val recursive_definition :
bool ->
Names.Id.t ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 10:02:09 +0000