aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/FunInd.v10
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/functional_principles_proofs.ml3
-rw-r--r--plugins/funind/functional_principles_proofs.mli4
-rw-r--r--plugins/funind/functional_principles_types.ml8
-rw-r--r--plugins/funind/functional_principles_types.mli2
-rw-r--r--plugins/funind/glob_term_to_relation.ml8
-rw-r--r--plugins/funind/glob_termops.ml2
-rw-r--r--plugins/funind/indfun.ml82
-rw-r--r--plugins/funind/indfun.mli2
-rw-r--r--plugins/funind/indfun_common.ml4
-rw-r--r--plugins/funind/indfun_common.mli4
-rw-r--r--plugins/funind/invfun.ml10
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml4
-rw-r--r--plugins/funind/recdef.mli4
16 files changed, 78 insertions, 73 deletions
diff --git a/plugins/funind/FunInd.v b/plugins/funind/FunInd.v
new file mode 100644
index 0000000000..e40aea7764
--- /dev/null
+++ b/plugins/funind/FunInd.v
@@ -0,0 +1,10 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+Require Coq.extraction.Extraction.
+Declare ML Module "recdef_plugin".
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index e4433247b4..64f43b8335 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -6,8 +6,8 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
+Require Export Coq.funind.FunInd.
Require Import PeanoNat.
-
Require Compare_dec.
Require Wf_nat.
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index ef894b2395..ba46f78aa8 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -10,7 +10,6 @@ open Names
open Pp
open Tacmach
open Termops
-open Proof_type
open Tacticals
open Tactics
open Indfun_common
@@ -106,7 +105,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
}
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 5bb288678d..d03fc475e0 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -4,7 +4,7 @@ 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 +14,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 70245a8b1e..8ffd15f9fb 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -371,12 +371,12 @@ let generate_functional_principle (evd: Evd.evar_map ref)
begin
begin
try
- let id = Pfedit.get_current_proof_name () in
+ let id = Proof_global.get_current_proof_name () in
let s = Id.to_string id in
let n = String.length "___________princ_________" in
if String.length s >= n
then if String.equal (String.sub s 0 n) "___________princ_________"
- then Pfedit.delete_current_proof ()
+ then Proof_global.discard_current ()
else ()
else ()
with e when CErrors.noncritical e -> ()
@@ -524,12 +524,12 @@ let make_scheme evd (fas : (pconstant*glob_sort) list) : Safe_typing.private_con
begin
begin
try
- let id = Pfedit.get_current_proof_name () in
+ let id = Proof_global.get_current_proof_name () in
let s = Id.to_string id in
let n = String.length "___________princ_________" in
if String.length s >= n
then if String.equal (String.sub s 0 n) "___________princ_________"
- then Pfedit.delete_current_proof ()
+ then Proof_global.discard_current ()
else ()
else ()
with e when CErrors.noncritical e -> ()
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index bb2b2d9186..e70ef23656 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -28,7 +28,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/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 0e2ca49000..db2af2be53 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1459,7 +1459,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 +1472,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 +1487,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_termops.ml b/plugins/funind/glob_termops.ml
index a7481370a3..726a8203d7 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -722,7 +722,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect
(* we first (pseudo) understand [rt] and get back the computed evar_map *)
(* FIXME : JF (30/03/2017) I'm not completely sure to have split understand as needed.
If someone knows how to prevent solved existantial removal in understand, please do not hesitate to change the computation of [ctx] here *)
- let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Pretyping.empty_lvar expected_type rt in
+ let ctx,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
let ctx, f = Evarutil.nf_evars_and_universes ctx in
(* then we map [rt] to replace the implicit holes by their values *)
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d12aa7f425..2c5dae1cde 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -343,7 +343,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 +446,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 +576,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 +623,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
diff --git a/plugins/funind/indfun.mli b/plugins/funind/indfun.mli
index 33420d8132..fc7da6a338 100644
--- a/plugins/funind/indfun.mli
+++ b/plugins/funind/indfun.mli
@@ -16,7 +16,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 7558ac7ac2..6fe6888f3d 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -161,7 +161,7 @@ let save with_clean id const (locality,_,kind) hook =
let kn = declare_constant id ~local (DefinitionEntry const, k) in
(locality, ConstRef kn)
in
- if with_clean then Pfedit.delete_current_proof ();
+ if with_clean then Proof_global.discard_current ();
CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
definition_message id
@@ -173,7 +173,7 @@ let cook_proof _ =
let get_proof_clean do_reduce =
let result = cook_proof do_reduce in
- Pfedit.delete_current_proof ();
+ Proof_global.discard_current ();
result
let with_full_print f a =
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 6b40c91713..f7a9cedd73 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -105,7 +105,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 +114,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..94ef2590c8 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -218,7 +218,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 +468,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 +629,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 +673,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 +953,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..ba88563d3b 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -880,7 +880,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 20abde82f2..8e12b239e8 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -30,7 +30,7 @@ open Nametab
open Declare
open Decl_kinds
open Tacred
-open Proof_type
+open Goal
open Pfedit
open Glob_term
open Pretyping
@@ -1295,7 +1295,7 @@ let is_opaque_constant c =
let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
(* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
- let current_proof_name = get_current_proof_name () in
+ let current_proof_name = Proof_global.get_current_proof_name () in
let name = match goal_name with
| Some s -> s
| None ->
diff --git a/plugins/funind/recdef.mli b/plugins/funind/recdef.mli
index e1a072799e..f3d5e73320 100644
--- a/plugins/funind/recdef.mli
+++ b/plugins/funind/recdef.mli
@@ -2,10 +2,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-02-10 05:28:48 +0000