aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--.depend26
-rw-r--r--.depend.camlp42
-rw-r--r--CHANGES10
-rw-r--r--parsing/g_tactic.ml425
-rw-r--r--parsing/pcoq.ml45
-rw-r--r--parsing/pcoq.mli5
-rw-r--r--proofs/logic.ml57
-rw-r--r--proofs/proof_trees.ml6
-rw-r--r--proofs/proof_type.ml8
-rw-r--r--proofs/proof_type.mli8
-rw-r--r--proofs/tacinterp.ml17
-rw-r--r--proofs/tacmach.ml18
-rw-r--r--proofs/tacmach.mli9
-rw-r--r--tactics/elim.ml26
-rw-r--r--tactics/elim.mli2
-rw-r--r--tactics/hiddentac.ml2
-rw-r--r--tactics/tactics.ml21
-rw-r--r--tactics/tactics.mli32
18 files changed, 204 insertions, 75 deletions
diff --git a/.depend b/.depend
index d7c1472ced..5e7ab5e0e8 100644
--- a/.depend
+++ b/.depend
@@ -983,16 +983,16 @@ tactics/eauto.cmx: tactics/auto.cmx proofs/clenv.cmx proofs/evar_refiner.cmx \
proofs/proof_type.cmx kernel/reduction.cmx kernel/sign.cmx \
proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
kernel/term.cmx lib/util.cmx
-tactics/elim.cmo: proofs/clenv.cmi tactics/hiddentac.cmi \
- tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi lib/pp.cmi \
- proofs/proof_type.cmi kernel/reduction.cmi proofs/tacmach.cmi \
- tactics/tacticals.cmi tactics/tactics.cmi kernel/term.cmi lib/util.cmi \
- tactics/elim.cmi
-tactics/elim.cmx: proofs/clenv.cmx tactics/hiddentac.cmx \
- tactics/hipattern.cmx kernel/inductive.cmx kernel/names.cmx lib/pp.cmx \
- proofs/proof_type.cmx kernel/reduction.cmx proofs/tacmach.cmx \
- tactics/tacticals.cmx tactics/tactics.cmx kernel/term.cmx lib/util.cmx \
- tactics/elim.cmi
+tactics/elim.cmo: proofs/clenv.cmi library/declare.cmi tactics/hiddentac.cmi \
+ tactics/hipattern.cmi kernel/inductive.cmi kernel/names.cmi \
+ library/nametab.cmi lib/pp.cmi proofs/proof_type.cmi kernel/reduction.cmi \
+ proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi \
+ kernel/term.cmi lib/util.cmi tactics/elim.cmi
+tactics/elim.cmx: proofs/clenv.cmx library/declare.cmx tactics/hiddentac.cmx \
+ tactics/hipattern.cmx kernel/inductive.cmx kernel/names.cmx \
+ library/nametab.cmx lib/pp.cmx proofs/proof_type.cmx kernel/reduction.cmx \
+ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx \
+ kernel/term.cmx lib/util.cmx tactics/elim.cmi
tactics/eqdecide.cmo: tactics/auto.cmi parsing/coqlib.cmi \
tactics/equality.cmi library/global.cmi tactics/hiddentac.cmi \
tactics/hipattern.cmi kernel/names.cmi pretyping/pattern.cmi \
@@ -1127,6 +1127,12 @@ tactics/tactics.cmx: parsing/astterm.cmx proofs/clenv.cmx kernel/closure.cmx \
kernel/reduction.cmx kernel/sign.cmx lib/stamps.cmx proofs/tacinterp.cmx \
proofs/tacmach.cmx pretyping/tacred.cmx tactics/tacticals.cmx \
kernel/term.cmx lib/util.cmx tactics/tactics.cmi
+tactics/tauto.cmo: parsing/ast.cmi parsing/coqast.cmi tactics/hipattern.cmi \
+ kernel/names.cmi lib/pp.cmi proofs/proof_type.cmi proofs/tacinterp.cmi \
+ proofs/tacmach.cmi tactics/tacticals.cmi tactics/tactics.cmi lib/util.cmi
+tactics/tauto.cmx: parsing/ast.cmx parsing/coqast.cmx tactics/hipattern.cmx \
+ kernel/names.cmx lib/pp.cmx proofs/proof_type.cmx proofs/tacinterp.cmx \
+ proofs/tacmach.cmx tactics/tacticals.cmx tactics/tactics.cmx lib/util.cmx
tactics/termdn.cmo: tactics/dn.cmi kernel/names.cmi pretyping/pattern.cmi \
pretyping/rawterm.cmi kernel/term.cmi lib/util.cmi tactics/termdn.cmi
tactics/termdn.cmx: tactics/dn.cmx kernel/names.cmx pretyping/pattern.cmx \
diff --git a/.depend.camlp4 b/.depend.camlp4
index 6612744a1c..ac3ad8320d 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,4 +1,4 @@
-tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_constr.cmo
+tactics/tauto.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
contrib/correctness/psyntax.ml: parsing/grammar.cma
contrib/field/field.ml: parsing/grammar.cma kernel/names.cmo parsing/ast.cmo parsing/g_tactic.cmo parsing/g_ltac.cmo parsing/g_constr.cmo
parsing/lexer.ml:
diff --git a/CHANGES b/CHANGES
index 3b1e5bd1eb..a909449f67 100644
--- a/CHANGES
+++ b/CHANGES
@@ -1,3 +1,13 @@
+Modifications depuis la V7.0
+
+- Fonctions de réduction dans les définitions locales s'appliquent par
+ défaut au corps de la définition. Extension de la notion de Clause
+ pour forcer l'action sur le type des défs seulement sous la forme
+ "Change c in Type of H."
+- Prise en compte des qualid dans Decompose
+- Correction bug inférence type Cases en présence de K-rédex
+- Correction bugs Cases en cas de prédicat dépendant
+
Différences V7.0beta / V7.0
- Portage de Correctness
- Réécriture de Extraction
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 70aaba18d1..c374f59557 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -54,6 +54,9 @@ GEXTEND Gram
[ [ id = Constr.ident -> id
| "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >> ] ]
;
+ idmetahyp:
+ [ [ id = idmeta_arg -> <:ast< (INHYP $id) >> ] ]
+ ;
qualidarg:
[ [ l = Constr.qualid -> <:ast< (QUALIDARG ($LIST l)) >>
| "?"; n = Prim.number -> <:ast< (QUALIDMETA $n) >> ] ]
@@ -94,8 +97,8 @@ GEXTEND Gram
ne_identarg_list:
[ [ l = LIST1 identarg -> l ] ]
;
- ne_idmeta_arg_list:
- [ [ l = LIST1 idmeta_arg -> l ] ]
+ ne_idmetahyp_list:
+ [ [ l = LIST1 idmetahyp -> l ] ]
;
ne_qualidarg_list:
[ [ l = LIST1 qualidarg -> l ] ]
@@ -211,8 +214,15 @@ GEXTEND Gram
| IDENT "Pattern"; pl = ne_pattern_list ->
<:ast< (Pattern ($LIST $pl)) >> ] ]
;
+ hypident:
+ [ [ id = identarg -> <:ast< (INHYP $id) >>
+ | "("; "Type"; "of"; id = identarg; ")" -> <:ast< (INHYPTYPE $id) >> ] ]
+ ;
+ ne_hyp_list:
+ [ [ l = LIST1 hypident -> l ] ]
+ ;
clausearg:
- [ [ "in"; idl = ne_identarg_list -> <:ast< (CLAUSE ($LIST idl)) >>
+ [ [ "in"; idl = ne_hyp_list -> <:ast< (CLAUSE ($LIST idl)) >>
| -> <:ast< (CLAUSE) >> ] ]
;
fixdecl:
@@ -225,9 +235,6 @@ GEXTEND Gram
<:ast< (COFIXEXP $id $c) >> :: fd
| -> [] ] ]
;
- END
-
-GEXTEND Gram
simple_tactic:
[ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >>
| IDENT "Fix"; id = identarg; n = pure_numarg -> <:ast< (Fix $id $n) >>
@@ -300,8 +307,8 @@ GEXTEND Gram
<:ast< (DecomposeAnd $c) >>
| IDENT "Decompose"; IDENT "Sum"; c = constrarg ->
<:ast< (DecomposeOr $c) >>
- | IDENT "Decompose"; "["; l = ne_identarg_list; "]"; c = constrarg ->
- <:ast< (DecomposeThese (CLAUSE ($LIST $l)) $c) >>
+ | IDENT "Decompose"; "["; l = ne_qualidarg_list; "]"; c = constrarg ->
+ <:ast< (DecomposeThese $c ($LIST $l)) >>
| IDENT "Cut"; c = constrarg -> <:ast< (Cut $c) >>
| IDENT "Specialize"; n = pure_numarg; lcb = constrarg_binding_list ->
<:ast< (Specialize $n ($LIST $lcb))>>
@@ -314,7 +321,7 @@ GEXTEND Gram
| IDENT "LetTac"; s = identarg; ":="; c = constrarg; p = clause_pattern->
<:ast< (LetTac $s $c $p) >>
| IDENT "LApply"; c = constrarg -> <:ast< (CutAndApply $c) >>
- | IDENT "Clear"; l = ne_idmeta_arg_list ->
+ | IDENT "Clear"; l = ne_idmetahyp_list ->
<:ast< (Clear (CLAUSE ($LIST $l))) >>
| IDENT "Move"; id1 = identarg; IDENT "after"; id2 = identarg ->
<:ast< (MoveDep $id1 $id2) >>
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index ff103ae2ca..849d2639cc 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -292,7 +292,9 @@ module Tactic =
let constrarg_list = gec_list "constrarg_list"
let ident_or_constrarg = gec "ident_or_constrarg"
let identarg = gec "identarg"
+ let hypident = gec "hypident"
let idmeta_arg = gec "idmeta_arg"
+ let idmetahyp = gec "idmetahyp"
let qualidarg = gec "qualidarg"
let qualidconstarg = gec "qualidconstarg"
let input_fun = gec "input_fun"
@@ -307,7 +309,8 @@ module Tactic =
let match_rule = gec "match_rule"
let match_list = gec_list "match_list"
let ne_identarg_list = gec_list "ne_identarg_list"
- let ne_idmeta_arg_list = gec_list "ne_idmeta_arg_list"
+ let ne_hyp_list = gec_list "ne_hyp_list"
+ let ne_idmetahyp_list = gec_list "ne_idmetahyp_list"
let ne_qualidarg_list = gec_list "ne_qualidarg_list"
let ne_qualidconstarg_list = gec_list "ne_qualidconstarg_list"
let ne_pattern_list = gec_list "ne_pattern_list"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index 30773eaa6a..b9c77509e2 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -116,7 +116,9 @@ module Tactic :
val fixdecl : Coqast.t list Gram.Entry.e
val ident_or_constrarg : Coqast.t Gram.Entry.e
val identarg : Coqast.t Gram.Entry.e
+ val hypident : Coqast.t Gram.Entry.e
val idmeta_arg : Coqast.t Gram.Entry.e
+ val idmetahyp : Coqast.t Gram.Entry.e
val qualidarg : Coqast.t Gram.Entry.e
val qualidconstarg : Coqast.t Gram.Entry.e
val input_fun : Coqast.t Gram.Entry.e
@@ -132,7 +134,8 @@ module Tactic :
val match_rule : Coqast.t Gram.Entry.e
val match_list : Coqast.t list Gram.Entry.e
val ne_identarg_list : Coqast.t list Gram.Entry.e
- val ne_idmeta_arg_list : Coqast.t list Gram.Entry.e
+ val ne_hyp_list : Coqast.t list Gram.Entry.e
+ val ne_idmetahyp_list : Coqast.t list Gram.Entry.e
val ne_qualidarg_list : Coqast.t list Gram.Entry.e
val ne_qualidconstarg_list : Coqast.t list Gram.Entry.e
val ne_intropattern : Coqast.t Gram.Entry.e
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 3f22a6f8ba..a5fe2d5962 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -266,13 +266,37 @@ let check_forward_dependencies id tail =
^ (string_of_id id')))
tail
-let convert_hyp sign sigma id ty =
+let convert_hyp sign sigma id b =
apply_to_hyp sign id
(fun sign (idc,c,ct) _ ->
let env = Global.env_of_context sign in
- if !check && not (is_conv env sigma ty (body_of_type ct)) then
- error "convert-hyp rule passed non-converting term";
- add_named_decl (idc,c,ty) sign)
+ match c with
+ | None -> (* Change the type *)
+ if !check && not (is_conv env sigma b ct) then
+ error "convert-hyp rule passed non-converting term";
+ add_named_decl (idc,c,b) sign
+ | Some c -> (* Change the body *)
+ if !check && not (is_conv env sigma b c) then
+ error "convert-hyp rule passed non-converting term";
+ add_named_decl (idc,Some b,ct) sign)
+
+let convert_def inbody sign sigma id c =
+ apply_to_hyp sign id
+ (fun sign (idc,b,t) _ ->
+ let env = Global.env_of_context sign in
+ match b with
+ | None -> error "convert-deftype rule passed to an hyp without body"
+ | Some b ->
+ let b,t =
+ if inbody then
+ (if !check && not (is_conv env sigma c b) then
+ error "convert-deftype rule passed non-converting type";
+ (c,t))
+ else
+ (if !check && not (is_conv env sigma c t) then
+ error "convert-deftype rule passed non-converting type";
+ (b,c)) in
+ add_named_decl (idc,Some b,t) sign)
let replace_hyp sign id d =
apply_to_hyp sign id
@@ -445,8 +469,14 @@ let prim_refiner r sigma goal =
else
error "convert-concl rule passed non-converting term"
- | { name = Convert_hyp; hypspecs = [id]; terms = [ty'] } ->
- [mk_goal info (convert_hyp sign sigma id ty') cl]
+ | { name = Convert_hyp; hypspecs = [id]; terms = [ty] } ->
+ [mk_goal info (convert_hyp sign sigma id ty) cl]
+
+ | { name = Convert_defbody; hypspecs = [id]; terms = [c] } ->
+ [mk_goal info (convert_def true sign sigma id c) cl]
+
+ | { name = Convert_deftype; hypspecs = [id]; terms = [ty] } ->
+ [mk_goal info (convert_def false sign sigma id ty) cl]
| { name = Thin; hypspecs = ids } ->
let clear_aux sign id =
@@ -537,7 +567,13 @@ let prim_extractor subfun vl pft =
| {ref=Some(Prim{name=Convert_concl;terms=[c]},[pf])} ->
subfun vl pf
- | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[c]},[pf])} ->
+ | {ref=Some(Prim{name=Convert_hyp;hypspecs=[id];terms=[_]},[pf])} ->
+ subfun vl pf
+
+ | {ref=Some(Prim{name=Convert_defbody;hypspecs=[id];terms=[_]},[pf])} ->
+ subfun vl pf
+
+ | {ref=Some(Prim{name=Convert_deftype;hypspecs=[id];terms=[_]},[pf])} ->
subfun vl pf
| {ref=Some(Prim{name=Thin;hypspecs=ids},[pf])} ->
@@ -600,6 +636,13 @@ let pr_prim_rule = function
| {name=Convert_hyp;hypspecs=[id];terms=[c]} ->
[< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >]
+ | {name=Convert_defbody;hypspecs=[id];terms=[c]} ->
+ [< 'sTR"Change " ; prterm c ; 'sPC ; 'sTR"in " ; pr_id id >]
+
+ | {name=Convert_deftype;hypspecs=[id];terms=[c]} ->
+ [< 'sTR"Change " ; prterm c ; 'sPC ;
+ 'sTR"in (Type of " ; pr_id id; 'sTR ")" >]
+
| {name=Thin;hypspecs=ids} ->
[< 'sTR"Clear " ; prlist_with_sep pr_spc pr_id ids >]
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 18cd475cde..45fe9e5a47 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -407,7 +407,11 @@ let ast_of_cvt_arg = function
| Constr_context _ ->
anomalylabstrm "ast_of_cvt_arg" [<'sTR
"Constr_context argument could not be used">]
- | Clause idl -> ope ("CLAUSE", List.map (compose nvar string_of_id) idl)
+ | Clause idl ->
+ let transl = function
+ | InHyp id -> ope ("INHYP", [nvar (string_of_id id)])
+ | InHypType id -> ope ("INHYPTYPE", [nvar (string_of_id id)]) in
+ ope ("CLAUSE", List.map transl idl)
| Bindings bl -> ope ("BINDINGS",
List.map (ast_of_cvt_bind (fun x -> x)) bl)
| Cbindings bl ->
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index bf8deb53a5..363dd09645 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -28,6 +28,10 @@ type pf_status =
| Complete_proof
| Incomplete_proof
+type hyp_location = (* To distinguish body and type of local defs *)
+ | InHyp of identifier
+ | InHypType of identifier
+
type prim_rule_name =
| Intro
| Intro_after
@@ -37,6 +41,8 @@ type prim_rule_name =
| Refine
| Convert_concl
| Convert_hyp
+ | Convert_defbody
+ | Convert_deftype
| Thin
| Move of bool
@@ -97,7 +103,7 @@ and tactic_arg =
| Identifier of identifier
| Qualid of Nametab.qualid
| Integer of int
- | Clause of identifier list
+ | Clause of hyp_location list
| Bindings of Coqast.t substitution
| Cbindings of constr substitution
| Quoted_string of string
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index de2c155f07..5d415d5a08 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -31,6 +31,10 @@ type pf_status =
| Complete_proof
| Incomplete_proof
+type hyp_location = (* To distinguish body and type of local defs *)
+ | InHyp of identifier
+ | InHypType of identifier
+
type prim_rule_name =
| Intro
| Intro_after
@@ -40,6 +44,8 @@ type prim_rule_name =
| Refine
| Convert_concl
| Convert_hyp
+ | Convert_defbody
+ | Convert_deftype
| Thin
| Move of bool
@@ -129,7 +135,7 @@ and tactic_arg =
| Identifier of identifier
| Qualid of Nametab.qualid
| Integer of int
- | Clause of identifier list
+ | Clause of hyp_location list
| Bindings of Coqast.t substitution
| Cbindings of constr substitution
| Quoted_string of string
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index 4b45132455..35435f7a70 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -529,6 +529,10 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
| Invalid_argument "destVar" ->
user_err_loc (loc, "Tacinterp.val_interp",[<'sTR
"Metavariable "; 'iNT n; 'sTR " must be an identifier" >]))*)
+ | Node(loc,"QUALIDARG",p) -> VArg (Qualid (interp_qualid p))
+ | Node(loc,"QUALIDMETA",[Num(_,n)]) ->
+ VArg
+ (Qualid (Nametab.qualid_of_sp (path_of_const (List.assoc n lmatch))))
| Str(_,s) -> VArg (Quoted_string s)
| Num(_,n) -> VArg (Integer n)
| Node(_,"COMMAND",[c]) ->
@@ -544,8 +548,8 @@ let rec val_interp (evc,env,lfun,lmatch,goalopt,debug) ast =
VArg (Redexp (redexp_of_ast (evc,env,lfun,lmatch,goalopt,debug)
(redname,args)))
| Node(_,"CLAUSE",cl) ->
- VArg (Clause (List.map (fun ast -> make_ids ast (unvarg (val_interp
- (evc,env,lfun,lmatch,goalopt,debug) ast))) cl))
+ VArg (Clause (List.map (clause_interp
+ (evc,env,lfun,lmatch,goalopt,debug)) cl))
| Node(_,"TACTIC",[ast]) ->
VArg (Tac ((tac_interp lfun lmatch debug ast),ast))
(*Remains to treat*)
@@ -1170,7 +1174,14 @@ and cvt_letpattern (evc,env,lfun,lmatch,goalopt,debug) (o,l) = function
error "\"Goal\" occurs twice"
else
(Some (List.map num_of_ast nums), l)
- | arg -> invalid_arg_loc (Ast.loc arg,"cvt_hyppattern")
+ | arg -> invalid_arg_loc (Ast.loc arg,"cvt_letpattern")
+
+(* Interprets an hypothesis name *)
+and clause_interp info = function
+ | Node(_,("INHYP"|"INHYPTYPE" as where),[ast]) ->
+ let id = make_ids ast (unvarg (val_interp info ast)) in
+ if where = "INHYP" then InHyp id else InHypType id
+ | arg -> invalid_arg_loc (Ast.loc arg,"clause_interp")
(* Interprets tactic arguments *)
let interp_tacarg sign ast = unvarg (val_interp sign ast)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index b68196ff3b..d63325cd85 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -58,12 +58,14 @@ let pf_nth_hyp_id gls n = let (id,c,t) = List.nth (pf_hyps gls) (n-1) in id
let pf_last_hyp gl = List.hd (pf_hyps gl)
-let pf_get_hyp_typ gls id =
+let pf_get_hyp gls id =
try
- body_of_type (snd (lookup_id id (pf_hyps gls)))
+ lookup_id id (pf_hyps gls)
with Not_found ->
error ("No such hypothesis : " ^ (string_of_id id))
+let pf_get_hyp_typ gls id = snd (pf_get_hyp gls id)
+
let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
let pf_ctxt gls = get_ctxt (sig_it gls)
@@ -229,9 +231,17 @@ let convert_concl c pf =
refiner (Prim { name = Convert_concl; terms = [c];
hypspecs = []; newids = []; params = [] }) pf
-let convert_hyp id c pf =
+let convert_hyp id t pf =
refiner (Prim { name = Convert_hyp; hypspecs = [id];
- terms = [c]; newids = []; params = []}) pf
+ terms = [t]; newids = []; params = []}) pf
+
+let convert_defbody id t pf =
+ refiner (Prim { name = Convert_defbody; hypspecs = [id];
+ terms = [t]; newids = []; params = []}) pf
+
+let convert_deftype id t pf =
+ refiner (Prim { name = Convert_deftype; hypspecs = [id];
+ terms = [t]; newids = []; params = []}) pf
let thin ids gl =
refiner (Prim { name = Thin; hypspecs = ids;
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 5481491d53..e7742f2ecd 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -56,7 +56,8 @@ val hnf_type_of : goal sigma -> constr -> constr
val pf_interp_constr : goal sigma -> Coqast.t -> constr
val pf_interp_type : goal sigma -> Coqast.t -> constr
-val pf_get_hyp_typ : goal sigma -> identifier -> constr
+val pf_get_hyp : goal sigma -> identifier -> constr option * types
+val pf_get_hyp_typ : goal sigma -> identifier -> types
val pf_reduction_of_redexp : goal sigma -> red_expr -> constr -> constr
@@ -162,7 +163,9 @@ val introduction : identifier -> tactic
val intro_replacing : identifier -> tactic
val refine : constr -> tactic
val convert_concl : constr -> tactic
-val convert_hyp : identifier -> constr -> tactic
+val convert_hyp : identifier -> types -> tactic
+val convert_deftype : identifier -> types -> tactic
+val convert_defbody : identifier -> constr -> tactic
val thin : identifier list -> tactic
val move_hyp : bool -> identifier -> identifier -> tactic
val mutual_fix : identifier list -> int list -> constr list -> tactic
@@ -228,7 +231,7 @@ val hide_openconstr_tactic : Pretyping.open_constr hide_combinator
val hide_constrl_tactic : (constr list) hide_combinator
val hide_numarg_tactic : int hide_combinator
val hide_ident_tactic : identifier hide_combinator
-val hide_identl_tactic : (identifier list) hide_combinator
+val hide_identl_tactic : hyp_location list hide_combinator
val hide_string_tactic : string hide_combinator
val hide_bindl_tactic : ((bindOcc * constr) list) hide_combinator
val hide_cbindl_tactic : (constr * (bindOcc * constr) list) hide_combinator
diff --git a/tactics/elim.ml b/tactics/elim.ml
index ffe2ff0715..81a5cfc54c 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -97,15 +97,16 @@ let head_in gls indl t =
in List.mem ity indl
with Induc -> false
-let inductive_of_ident gls id =
- match kind_of_term (pf_global gls id) with
+let inductive_of_qualid gls qid =
+ let c = Declare.construct_qualified_reference (pf_env gls) qid in
+ match kind_of_term c with
| IsMutInd ity -> ity
| _ ->
errorlabstrm "Decompose"
- [< pr_id id; 'sTR " is not an inductive type" >]
+ [< Nametab.pr_qualid qid; 'sTR " is not an inductive type" >]
let decompose_these c l gls =
- let indl = List.map (inductive_of_ident gls) l in
+ let indl = List.map (inductive_of_qualid gls) l in
general_decompose (fun (_,t) -> head_in gls indl t) c gls
let decompose_nonrec c gls =
@@ -123,17 +124,22 @@ let decompose_or c gls =
(fun (_,t) -> is_disjunction t)
c gls
-let dyn_decompose args gl =
+let dyn_decompose args gl =
+ let out_qualid = function
+ | Qualid qid -> qid
+ | l -> bad_tactic_args "DecomposeThese" [l] gl in
match args with
- | [Clause ids; Command c] ->
- decompose_these (pf_interp_constr gl c) ids gl
- | [Clause ids; Constr c] ->
- decompose_these c ids gl
+ | Command c :: ids ->
+ decompose_these (pf_interp_constr gl c) (List.map out_qualid ids) gl
+ | Constr c :: ids ->
+ decompose_these c (List.map out_qualid ids) gl
| l -> bad_tactic_args "DecomposeThese" l gl
let h_decompose =
let v_decompose = hide_tactic "DecomposeThese" dyn_decompose in
- fun ids c -> v_decompose [Clause ids; Constr c]
+ fun ids c ->
+ v_decompose
+ (Constr c :: List.map (fun x -> Qualid (Nametab.qualid_of_sp x)) ids)
let vernac_decompose_and =
hide_constr_tactic "DecomposeAnd" decompose_and
diff --git a/tactics/elim.mli b/tactics/elim.mli
index e2b9a75e35..c21d4452b9 100644
--- a/tactics/elim.mli
+++ b/tactics/elim.mli
@@ -29,7 +29,7 @@ val general_decompose : (clause * constr -> bool) -> constr -> tactic
val decompose_nonrec : constr -> tactic
val decompose_and : constr -> tactic
val decompose_or : constr -> tactic
-val h_decompose : identifier list -> constr -> tactic
+val h_decompose : section_path list -> constr -> tactic
val double_ind : int -> int -> tactic
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml
index 2c4f80b748..bc07c9a4d6 100644
--- a/tactics/hiddentac.ml
+++ b/tactics/hiddentac.ml
@@ -13,7 +13,7 @@ open Proof_type
open Tacmach
open Tacentries
-let h_clear ids = v_clear [(Clause ids)]
+let h_clear ids = v_clear [(Clause (List.map (fun x -> InHyp x) ids))]
let h_move dep id1 id2 =
(if dep then v_move else v_move_dep) [Identifier id1;Identifier id2]
let h_contradiction = v_contradiction []
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 2d68a721f0..0e454846a0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -152,11 +152,20 @@ type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr
let reduct_in_concl redfun gl =
convert_concl (pf_reduce redfun gl (pf_concl gl)) gl
-let reduct_in_hyp redfun id gl =
- let ty = pf_get_hyp_typ gl id in
+let reduct_in_hyp redfun idref gl =
+ let inhyp,id = match idref with
+ | InHyp id -> true, id
+ | InHypType id -> false, id in
+ let c, ty = pf_get_hyp gl id in
let redfun' = under_casts (pf_reduce redfun gl) in
- convert_hyp id (redfun' ty) gl
-
+ match c with
+ | None -> convert_hyp id (redfun' ty) gl
+ | Some b ->
+ if inhyp then (* Default for defs: reduce in body *)
+ convert_defbody id (redfun' b) gl
+ else
+ convert_deftype id (redfun' ty) gl
+
let reduct_option redfun = function
| Some id -> reduct_in_hyp redfun id
| None -> reduct_in_concl redfun
@@ -783,7 +792,9 @@ let dyn_assumption = function
let clear ids gl = thin ids gl
let clear_one id gl = clear [id] gl
let dyn_clear = function
- | [Clause ids] -> clear ids
+ | [Clause ids] ->
+ let out = function InHyp id -> id | _ -> assert false in
+ clear (List.map out ids)
| _ -> assert false
(* Clears a list of identifiers clauses form the context *)
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 07db3b4590..6f315f358b 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -102,39 +102,39 @@ val dyn_exact_check : tactic_arg list -> tactic
type 'a tactic_reduction = env -> enamed_declarations -> constr -> constr
-val reduct_in_hyp : 'a tactic_reduction -> identifier -> tactic
-val reduct_option : 'a tactic_reduction -> identifier option -> tactic
+val reduct_in_hyp : 'a tactic_reduction -> hyp_location -> tactic
+val reduct_option : 'a tactic_reduction -> hyp_location option -> tactic
val reduct_in_concl : 'a tactic_reduction -> tactic
val change_in_concl : constr -> tactic
-val change_in_hyp : constr -> identifier -> tactic
-val change_option : constr -> identifier option -> tactic
+val change_in_hyp : constr -> hyp_location -> tactic
+val change_option : constr -> hyp_location option -> tactic
val red_in_concl : tactic
-val red_in_hyp : identifier -> tactic
-val red_option : identifier option -> tactic
+val red_in_hyp : hyp_location -> tactic
+val red_option : hyp_location option -> tactic
val hnf_in_concl : tactic
-val hnf_in_hyp : identifier -> tactic
-val hnf_option : identifier option -> tactic
+val hnf_in_hyp : hyp_location -> tactic
+val hnf_option : hyp_location option -> tactic
val simpl_in_concl : tactic
-val simpl_in_hyp : identifier -> tactic
-val simpl_option : identifier option -> tactic
+val simpl_in_hyp : hyp_location -> tactic
+val simpl_option : hyp_location option -> tactic
val normalise_in_concl: tactic
-val normalise_in_hyp : identifier -> tactic
-val normalise_option : identifier option -> tactic
+val normalise_in_hyp : hyp_location -> tactic
+val normalise_option : hyp_location option -> tactic
val unfold_in_concl : (int list * Closure.evaluable_global_reference) list
-> tactic
val unfold_in_hyp :
- (int list * Closure.evaluable_global_reference) list -> identifier -> tactic
+ (int list * Closure.evaluable_global_reference) list -> hyp_location -> tactic
val unfold_option :
- (int list * Closure.evaluable_global_reference) list -> identifier option
+ (int list * Closure.evaluable_global_reference) list -> hyp_location option
-> tactic
-val reduce : red_expr -> identifier list -> tactic
+val reduce : red_expr -> hyp_location list -> tactic
val dyn_reduce : tactic_arg list -> tactic
val dyn_change : tactic_arg list -> tactic
val unfold_constr : global_reference -> tactic
val pattern_option :
- (int list * constr * constr) list -> identifier option -> tactic
+ (int list * constr * constr) list -> hyp_location option -> tactic
(*s Modification of the local context. *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-06 00:07:03 +0000