aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_coqast.ml410
-rw-r--r--intf/tacexpr.mli6
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--plugins/funind/functional_principles_proofs.ml2
-rw-r--r--printing/pptactic.ml6
-rw-r--r--tactics/hiddentac.ml4
-rw-r--r--tactics/hiddentac.mli5
-rw-r--r--tactics/tacinterp.ml24
-rw-r--r--toplevel/lemmas.ml4
9 files changed, 29 insertions, 36 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index cbbc9e187..4fe6d6aa1 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -335,22 +335,20 @@ let rec mlexpr_of_atomic_tactic = function
let ido = mlexpr_of_ident_option ido in
let n = mlexpr_of_int n in
<:expr< Tacexpr.TacFix $ido$ $n$ >>
- | Tacexpr.TacMutualFix (b,id,n,l) ->
- let b = mlexpr_of_bool b in
+ | Tacexpr.TacMutualFix (id,n,l) ->
let id = mlexpr_of_ident id in
let n = mlexpr_of_int n in
let f =mlexpr_of_triple mlexpr_of_ident mlexpr_of_int mlexpr_of_constr in
let l = mlexpr_of_list f l in
- <:expr< Tacexpr.TacMutualFix $b$ $id$ $n$ $l$ >>
+ <:expr< Tacexpr.TacMutualFix $id$ $n$ $l$ >>
| Tacexpr.TacCofix ido ->
let ido = mlexpr_of_ident_option ido in
<:expr< Tacexpr.TacCofix $ido$ >>
- | Tacexpr.TacMutualCofix (b,id,l) ->
- let b = mlexpr_of_bool b in
+ | Tacexpr.TacMutualCofix (id,l) ->
let id = mlexpr_of_ident id in
let f = mlexpr_of_pair mlexpr_of_ident mlexpr_of_constr in
let l = mlexpr_of_list f l in
- <:expr< Tacexpr.TacMutualCofix $b$ $id$ $l$ >>
+ <:expr< Tacexpr.TacMutualCofix $id$ $l$ >>
| Tacexpr.TacCut c ->
<:expr< Tacexpr.TacCut $mlexpr_of_constr c$ >>
diff --git a/intf/tacexpr.mli b/intf/tacexpr.mli
index 7da58ca09..18232dce0 100644
--- a/intf/tacexpr.mli
+++ b/intf/tacexpr.mli
@@ -28,7 +28,6 @@ type evars_flag = bool (* true = pose evars false = fail on evars *)
type rec_flag = bool (* true = recursive false = not recursive *)
type advanced_flag = bool (* true = advanced false = basic *)
type split_flag = bool (* true = exists false = split *)
-type hidden_flag = bool (* true = internal use false = user-level *)
type letin_flag = bool (* true = use local def false = use Leibniz *)
type debug = Debug | Info | Off (* for trivial / auto / eauto ... *)
@@ -106,10 +105,9 @@ type ('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_atomic_tactic_expr =
| TacCase of evars_flag * 'trm with_bindings
| TacCaseType of 'trm
| TacFix of identifier option * int
- | TacMutualFix of
- hidden_flag * identifier * int * (identifier * int * 'trm) list
+ | TacMutualFix of identifier * int * (identifier * int * 'trm) list
| TacCofix of identifier option
- | TacMutualCofix of hidden_flag * identifier * (identifier * 'trm) list
+ | TacMutualCofix of identifier * (identifier * 'trm) list
| TacCut of 'trm
| TacAssert of
('trm,'pat,'cst,'ind,'ref,'nam,'lev) gen_tactic_expr option *
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b21711d32..a60d9c966 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -537,11 +537,11 @@ GEXTEND Gram
| "fix"; n = natural -> TacFix (None,n)
| "fix"; id = ident; n = natural -> TacFix (Some id,n)
| "fix"; id = ident; n = natural; "with"; fd = LIST1 fixdecl ->
- TacMutualFix (false,id,n,List.map mk_fix_tac fd)
+ TacMutualFix (id,n,List.map mk_fix_tac fd)
| "cofix" -> TacCofix None
| "cofix"; id = ident -> TacCofix (Some id)
| "cofix"; id = ident; "with"; fd = LIST1 cofixdecl ->
- TacMutualCofix (false,id,List.map mk_cofix_tac fd)
+ TacMutualCofix (id,List.map mk_cofix_tac fd)
| IDENT "pose"; (id,b) = bindings_with_parameters ->
TacLetTac (Names.Name id,b,Locusops.nowhere,true,None)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 52b4d881a..f431e04d8 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1206,7 +1206,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
then
(* observe_tac ("h_fix") *) (h_fix (Some this_fix_info.name) (this_fix_info.idx +1))
else
- h_mutual_fix false this_fix_info.name (this_fix_info.idx + 1)
+ h_mutual_fix this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos
| _ -> anomaly "Not a valid information"
in
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index 055f08d93..48a59be05 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -681,13 +681,11 @@ and pr_atom1 = function
hov 1 (str (with_evars ev "case") ++ spc () ++ pr_with_bindings cb)
| TacCaseType c -> hov 1 (str "casetype" ++ pr_constrarg c)
| TacFix (ido,n) -> hov 1 (str "fix" ++ pr_opt pr_id ido ++ pr_intarg n)
- | TacMutualFix (hidden,id,n,l) ->
- if hidden then str "idtac" (* should caught before! *) else
+ | TacMutualFix (id,n,l) ->
hov 1 (str "fix" ++ spc () ++ pr_id id ++ pr_intarg n ++ spc() ++
str"with " ++ prlist_with_sep spc pr_fix_tac l)
| TacCofix ido -> hov 1 (str "cofix" ++ pr_opt pr_id ido)
- | TacMutualCofix (hidden,id,l) ->
- if hidden then str "idtac" (* should be caught before! *) else
+ | TacMutualCofix (id,l) ->
hov 1 (str "cofix" ++ spc () ++ pr_id id ++ spc() ++
str"with " ++ prlist_with_sep spc pr_cofix_tac l)
| TacCut c -> hov 1 (str "cut" ++ pr_constrarg c)
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 57326a485..fc0f24fcd 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -28,10 +28,10 @@ let h_elim_type = elim_type
let h_case = general_case_analysis
let h_case_type = case_type
let h_fix = fix
-let h_mutual_fix b id n l = mutual_fix id n l 0
+let h_mutual_fix id n l = mutual_fix id n l 0
let h_cofix = cofix
-let h_mutual_cofix b id l = mutual_cofix id l 0
+let h_mutual_cofix id l = mutual_cofix id l 0
let h_cut = cut
let h_generalize_gen cl =
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index f7426c8f1..1199fe7a8 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -46,11 +46,10 @@ val h_elim_type : constr -> tactic
val h_case : evars_flag -> constr with_bindings -> tactic
val h_case_type : constr -> tactic
-val h_mutual_fix : hidden_flag -> identifier -> int ->
+val h_mutual_fix : identifier -> int ->
(identifier * int * constr) list -> tactic
val h_fix : identifier option -> int -> tactic
-val h_mutual_cofix : hidden_flag -> identifier ->
- (identifier * constr) list -> tactic
+val h_mutual_cofix : identifier -> (identifier * constr) list -> tactic
val h_cofix : identifier option -> tactic
val h_cut : constr -> tactic
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 07b1e437d..0f378464a 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -695,13 +695,13 @@ let rec intern_atomic lf ist x =
| TacCase (ev,cb) -> TacCase (ev,intern_constr_with_bindings ist cb)
| TacCaseType c -> TacCaseType (intern_type ist c)
| TacFix (idopt,n) -> TacFix (Option.map (intern_ident lf ist) idopt,n)
- | TacMutualFix (b,id,n,l) ->
+ | TacMutualFix (id,n,l) ->
let f (id,n,c) = (intern_ident lf ist id,n,intern_type ist c) in
- TacMutualFix (b,intern_ident lf ist id, n, List.map f l)
+ TacMutualFix (intern_ident lf ist id, n, List.map f l)
| TacCofix idopt -> TacCofix (Option.map (intern_ident lf ist) idopt)
- | TacMutualCofix (b,id,l) ->
+ | TacMutualCofix (id,l) ->
let f (id,c) = (intern_ident lf ist id,intern_type ist c) in
- TacMutualCofix (b,intern_ident lf ist id, List.map f l)
+ TacMutualCofix (intern_ident lf ist id, List.map f l)
| TacCut c -> TacCut (intern_type ist c)
| TacAssert (otac,ipat,c) ->
TacAssert (Option.map (intern_pure_tactic ist) otac,
@@ -2359,7 +2359,7 @@ and interp_atomic ist gl tac =
(tclEVARS sigma)
(h_case_type c_interp)
| TacFix (idopt,n) -> h_fix (Option.map (interp_fresh_ident ist env) idopt) n
- | TacMutualFix (b,id,n,l) ->
+ | TacMutualFix (id,n,l) ->
let f sigma (id,n,c) =
let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
sigma , (interp_fresh_ident ist env id,n,c_interp) in
@@ -2371,9 +2371,9 @@ and interp_atomic ist gl tac =
in
tclTHEN
(tclEVARS sigma)
- (h_mutual_fix b (interp_fresh_ident ist env id) n l_interp)
+ (h_mutual_fix (interp_fresh_ident ist env id) n l_interp)
| TacCofix idopt -> h_cofix (Option.map (interp_fresh_ident ist env) idopt)
- | TacMutualCofix (b,id,l) ->
+ | TacMutualCofix (id,l) ->
let f sigma (id,c) =
let (sigma,c_interp) = pf_interp_type ist { gl with sigma=sigma } c in
sigma , (interp_fresh_ident ist env id,c_interp) in
@@ -2385,7 +2385,7 @@ and interp_atomic ist gl tac =
in
tclTHEN
(tclEVARS sigma)
- (h_mutual_cofix b (interp_fresh_ident ist env id) l_interp)
+ (h_mutual_cofix (interp_fresh_ident ist env id) l_interp)
| TacCut c ->
let (sigma,c_interp) = pf_interp_type ist gl c in
tclTHEN
@@ -2848,11 +2848,11 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
| TacCase (ev,cb) -> TacCase (ev,subst_glob_with_bindings subst cb)
| TacCaseType c -> TacCaseType (subst_glob_constr subst c)
| TacFix (idopt,n) as x -> x
- | TacMutualFix (b,id,n,l) ->
- TacMutualFix(b,id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
+ | TacMutualFix (id,n,l) ->
+ TacMutualFix(id,n,List.map (fun (id,n,c) -> (id,n,subst_glob_constr subst c)) l)
| TacCofix idopt as x -> x
- | TacMutualCofix (b,id,l) ->
- TacMutualCofix (b,id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
+ | TacMutualCofix (id,l) ->
+ TacMutualCofix (id, List.map (fun (id,c) -> (id,subst_glob_constr subst c)) l)
| TacCut c -> TacCut (subst_glob_constr subst c)
| TacAssert (b,na,c) ->
TacAssert (Option.map (subst_tactic subst) b,na,subst_glob_constr subst c)
diff --git a/toplevel/lemmas.ml b/toplevel/lemmas.ml
index 1c8302c1a..747f5835f 100644
--- a/toplevel/lemmas.ml
+++ b/toplevel/lemmas.ml
@@ -260,7 +260,7 @@ let start_proof id kind c ?init_tac ?(compute_guard=[]) hook =
let rec_tac_initializer finite guard thms snl =
if finite then
match List.map (fun (id,(t,_)) -> (id,t)) thms with
- | (id,_)::l -> Hiddentac.h_mutual_cofix true id l
+ | (id,_)::l -> Hiddentac.h_mutual_cofix id l
| _ -> assert false
else
(* nl is dummy: it will be recomputed at Qed-time *)
@@ -268,7 +268,7 @@ let rec_tac_initializer finite guard thms snl =
| None -> List.map succ (List.map List.last guard)
| Some nl -> nl
in match List.map2 (fun (id,(t,_)) n -> (id,n,t)) thms nl with
- | (id,n,_)::l -> Hiddentac.h_mutual_fix true id n l
+ | (id,n,_)::l -> Hiddentac.h_mutual_fix id n l
| _ -> assert false
let start_proof_with_initialization kind recguard thms snl hook =
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-13 07:18:05 +0000