aboutsummaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/functional_principles_proofs.ml26
-rw-r--r--plugins/funind/g_indfun.mlg (renamed from plugins/funind/g_indfun.ml4)122
-rw-r--r--plugins/funind/indfun_common.mli2
-rw-r--r--plugins/funind/recdef.ml2
4 files changed, 92 insertions, 60 deletions
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index b12364d04a..98d68d3db7 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -638,11 +638,11 @@ let my_orelse tac1 tac2 g =
(* observe (str "using snd tac since : " ++ CErrors.print e); *)
tac2 g
-let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
+let instantiate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
let args = Array.of_list (List.map mkVar args_id) in
- let instanciate_one_hyp hid =
+ let instantiate_one_hyp hid =
my_orelse
- ( (* we instanciate the hyp if possible *)
+ ( (* we instantiate the hyp if possible *)
fun g ->
let prov_hid = pf_get_new_id hid g in
let c = mkApp(mkVar hid,args) in
@@ -678,7 +678,7 @@ let instanciate_hyps_with_args (do_prove:Id.t list -> tactic) hyps args_id =
tclTHENLIST
[
tclMAP (fun hyp_id -> h_reduce_with_zeta (Locusops.onHyp hyp_id)) hyps;
- tclMAP instanciate_one_hyp hyps;
+ tclMAP instantiate_one_hyp hyps;
(fun g ->
let all_g_hyps_id =
List.fold_right Id.Set.add (pf_ids_of_hyps g) Id.Set.empty
@@ -722,11 +722,11 @@ let build_proof
tclTHENLIST [Proofview.V82.of_tactic (Simple.case t);
(fun g' ->
let g'_nb_prod = nb_prod (project g') (pf_concl g') in
- let nb_instanciate_partial = g'_nb_prod - g_nb_prod in
+ let nb_instantiate_partial = g'_nb_prod - g_nb_prod in
observe_tac "treat_new_case"
(treat_new_case
ptes_infos
- nb_instanciate_partial
+ nb_instantiate_partial
(build_proof do_finalize)
t
dyn_infos)
@@ -760,7 +760,7 @@ let build_proof
nb_rec_hyps = List.length new_hyps
}
in
-(* observe_tac "Lambda" *) (instanciate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
+(* observe_tac "Lambda" *) (instantiate_hyps_with_args do_prove new_infos.rec_hyps [id]) g'
(* build_proof do_finalize new_infos g' *)
) g
| _ ->
@@ -1120,7 +1120,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
(full_params, (* real params *)
princ_params, (* the params of the principle which are not params of the function *)
- substl (* function instanciated with real params *)
+ substl (* function instantiated with real params *)
(List.map var_of_decl full_params)
f_body
)
@@ -1130,7 +1130,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let f_body = compose_lam f_ctxt_other f_body in
(princ_info.params, (* real params *)
[],(* all params are full params *)
- substl (* function instanciated with real params *)
+ substl (* function instantiated with real params *)
(List.map var_of_decl princ_info.params)
f_body
)
@@ -1321,7 +1321,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
(* str "args := " ++ prlist_with_sep spc Ppconstr.pr_id args_id *)
(* ); *)
- (* observe_tac "instancing" *) (instanciate_hyps_with_args prove_tac
+ (* observe_tac "instancing" *) (instantiate_hyps_with_args prove_tac
(List.rev_map id_of_decl princ_info.branches)
(List.rev args_id))
]
@@ -1371,7 +1371,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
do_prove
dyn_infos
in
- instanciate_hyps_with_args prove_tac
+ instantiate_hyps_with_args prove_tac
(List.rev_map id_of_decl princ_info.branches)
(List.rev args_id)
]
@@ -1728,8 +1728,8 @@ let prove_principle_for_gen
ptes_info
(body_info rec_hyps)
in
- (* observe_tac "instanciate_hyps_with_args" *)
- (instanciate_hyps_with_args
+ (* observe_tac "instantiate_hyps_with_args" *)
+ (instantiate_hyps_with_args
make_proof
(List.map (get_name %> Nameops.Name.get_id) princ_info.branches)
(List.rev args_ids)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.mlg
index a2d31780dd..857215751a 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.mlg
@@ -7,23 +7,28 @@
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+
+{
+
open Ltac_plugin
open Util
open Pp
open Constrexpr
open Indfun_common
open Indfun
-open Genarg
open Stdarg
open Tacarg
open Tactypes
-open Pcoq
open Pcoq.Prim
open Pcoq.Constr
open Pltac
+}
+
DECLARE PLUGIN "recdef_plugin"
+{
+
let pr_fun_ind_using prc prlc _ opt_c =
match opt_c with
| None -> mt ()
@@ -44,26 +49,27 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
let (_, b) = b env evd in
spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
+}
ARGUMENT EXTEND fun_ind_using
TYPED AS constr_with_bindings option
- PRINTED BY pr_fun_ind_using_typed
- RAW_TYPED AS constr_with_bindings_opt
- RAW_PRINTED BY pr_fun_ind_using
- GLOB_TYPED AS constr_with_bindings_opt
- GLOB_PRINTED BY pr_fun_ind_using
-| [ "using" constr_with_bindings(c) ] -> [ Some c ]
-| [ ] -> [ None ]
+ PRINTED BY { pr_fun_ind_using_typed }
+ RAW_PRINTED BY { pr_fun_ind_using }
+ GLOB_PRINTED BY { pr_fun_ind_using }
+| [ "using" constr_with_bindings(c) ] -> { Some c }
+| [ ] -> { None }
END
TACTIC EXTEND newfuninv
- [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] ->
- [
+| [ "functional" "inversion" quantified_hypothesis(hyp) reference_opt(fname) ] ->
+ {
Proofview.V82.tactic (Invfun.invfun hyp fname)
- ]
+ }
END
+{
+
let pr_intro_as_pat _prc _ _ pat =
match pat with
| Some pat ->
@@ -75,56 +81,70 @@ let out_disjunctive = CAst.map (function
| IntroAction (IntroOrAndPattern l) -> l
| _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected."))
-ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
-| [ "as" simple_intropattern(ipat) ] -> [ Some ipat ]
-| [] ->[ None ]
+}
+
+ARGUMENT EXTEND with_names TYPED AS intropattern option PRINTED BY { pr_intro_as_pat }
+| [ "as" simple_intropattern(ipat) ] -> { Some ipat }
+| [] -> { None }
END
+{
+
let functional_induction b c x pat =
Proofview.V82.tactic (functional_induction true c x (Option.map out_disjunctive pat))
+}
TACTIC EXTEND newfunind
- ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
- [
+| ["functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
+ {
let c = match cl with
| [] -> assert false
| [c] -> c
| c::cl -> EConstr.applist(c,cl)
in
- Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl ]
+ Extratactics.onSomeWithHoles (fun x -> functional_induction true c x pat) princl }
END
(***** debug only ***)
TACTIC EXTEND snewfunind
- ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
- [
+| ["soft" "functional" "induction" ne_constr_list(cl) fun_ind_using(princl) with_names(pat)] ->
+ {
let c = match cl with
| [] -> assert false
| [c] -> c
| c::cl -> EConstr.applist(c,cl)
in
- Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl ]
+ Extratactics.onSomeWithHoles (fun x -> functional_induction false c x pat) princl }
END
+{
let pr_constr_comma_sequence prc _ _ = prlist_with_sep pr_comma prc
+}
+
ARGUMENT EXTEND constr_comma_sequence'
- TYPED AS constr_list
- PRINTED BY pr_constr_comma_sequence
-| [ constr(c) "," constr_comma_sequence'(l) ] -> [ c::l ]
-| [ constr(c) ] -> [ [c] ]
+ TYPED AS constr list
+ PRINTED BY { pr_constr_comma_sequence }
+| [ constr(c) "," constr_comma_sequence'(l) ] -> { c::l }
+| [ constr(c) ] -> { [c] }
END
+{
+
let pr_auto_using prc _prlc _prt = Pptactic.pr_auto_using prc
+}
+
ARGUMENT EXTEND auto_using'
- TYPED AS constr_list
- PRINTED BY pr_auto_using
-| [ "using" constr_comma_sequence'(l) ] -> [ l ]
-| [ ] -> [ [] ]
+ TYPED AS constr list
+ PRINTED BY { pr_auto_using }
+| [ "using" constr_comma_sequence'(l) ] -> { l }
+| [ ] -> { [] }
END
+{
+
module Gram = Pcoq.Gram
module Vernac = Pvernac.Vernac_
module Tactic = Pltac
@@ -137,23 +157,29 @@ let (wit_function_rec_definition_loc : function_rec_definition_loc_argtype Genar
let function_rec_definition_loc =
Pcoq.create_generic_entry Pcoq.utactic "function_rec_definition_loc" (Genarg.rawwit wit_function_rec_definition_loc)
-GEXTEND Gram
+}
+
+GRAMMAR EXTEND Gram
GLOBAL: function_rec_definition_loc ;
function_rec_definition_loc:
- [ [ g = Vernac.rec_definition -> Loc.tag ~loc:!@loc g ]]
+ [ [ g = Vernac.rec_definition -> { Loc.tag ~loc g } ]]
;
END
+{
+
let () =
let raw_printer _ _ _ (loc,body) = Ppvernac.pr_rec_definition body in
Pptactic.declare_extra_vernac_genarg_pprule wit_function_rec_definition_loc raw_printer
+}
+
(* TASSI: n'importe quoi ! *)
VERNAC COMMAND EXTEND Function
- ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
- => [ let hard = List.exists (function
+| ["Function" ne_function_rec_definition_loc_list_sep(recsl,"with")]
+ => { let hard = List.exists (function
| _,((_,(_,(CMeasureRec _|CWfRec _)),_,_,_),_) -> true
| _,((_,(_,CStructRec),_,_,_),_) -> false) recsl in
match
@@ -162,20 +188,25 @@ VERNAC COMMAND EXTEND Function
with
| Vernacexpr.VtSideff ids, _ when hard ->
Vernacexpr.(VtStartProof ("Classic", GuaranteesOpacity, ids), VtLater)
- | x -> x ]
- -> [ do_generate_principle false (List.map snd recsl) ]
+ | x -> x }
+ -> { do_generate_principle false (List.map snd recsl) }
END
+{
+
let pr_fun_scheme_arg (princ_name,fun_name,s) =
Names.Id.print princ_name ++ str " :=" ++ spc() ++ str "Induction for " ++
Libnames.pr_qualid fun_name ++ spc() ++ str "Sort " ++
Termops.pr_sort_family s
+}
+
VERNAC ARGUMENT EXTEND fun_scheme_arg
-PRINTED BY pr_fun_scheme_arg
-| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> [ (princ_name,fun_name,s) ]
+PRINTED BY { pr_fun_scheme_arg }
+| [ ident(princ_name) ":=" "Induction" "for" reference(fun_name) "Sort" sort_family(s) ] -> { (princ_name,fun_name,s) }
END
+{
let warning_error names e =
let (e, _) = ExplainErr.process_vernac_interp_error (e, Exninfo.null) in
@@ -190,12 +221,13 @@ let warning_error names e =
warn_cannot_define_principle (names,error)
| _ -> raise e
+}
VERNAC COMMAND EXTEND NewFunctionalScheme
- ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
- => [ Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater ]
+| ["Functional" "Scheme" ne_fun_scheme_arg_list_sep(fas,"with") ]
+ => { Vernacexpr.VtSideff(List.map pi1 fas), Vernacexpr.VtLater }
->
- [
+ {
begin
try
Functional_principles_types.build_scheme fas
@@ -223,17 +255,17 @@ VERNAC COMMAND EXTEND NewFunctionalScheme
warning_error names e
end
- ]
+ }
END
(***** debug only ***)
VERNAC COMMAND EXTEND NewFunctionalCase
- ["Functional" "Case" fun_scheme_arg(fas) ]
- => [ Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater ]
- -> [ Functional_principles_types.build_case_scheme fas ]
+| ["Functional" "Case" fun_scheme_arg(fas) ]
+ => { Vernacexpr.VtSideff[pi1 fas], Vernacexpr.VtLater }
+ -> { Functional_principles_types.build_case_scheme fas }
END
(***** debug only ***)
VERNAC COMMAND EXTEND GenerateGraph CLASSIFIED AS QUERY
-["Generate" "graph" "for" reference(c)] -> [ make_graph (Smartlocate.global_with_alias c) ]
+| ["Generate" "graph" "for" reference(c)] -> { make_graph (Smartlocate.global_with_alias c) }
END
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 7e52ee224f..1b4c1248a5 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -46,7 +46,7 @@ val jmeq : unit -> EConstr.constr
val jmeq_refl : unit -> EConstr.constr
val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry -> Decl_kinds.goal_kind ->
- unit Lemmas.declaration_hook CEphemeron.key -> unit
+ Lemmas.declaration_hook CEphemeron.key -> unit
(* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
abort the proof
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 89dfb58017..9fa333c629 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1320,7 +1320,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp
| None ->
try add_suffix current_proof_name "_subproof"
with e when CErrors.noncritical e ->
- anomaly (Pp.str "open_new_goal with an unamed theorem.")
+ anomaly (Pp.str "open_new_goal with an unnamed theorem.")
in
let na = next_global_ident_away name Id.Set.empty in
if Termops.occur_existential sigma gls_type then
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 02:02:19 +0000