summaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
-rw-r--r--toplevel/auto_ind_decl.ml92
1 files changed, 39 insertions, 53 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 16ceffed..f4dab15f 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -1,13 +1,11 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auto_ind_decl.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
(* This file is about the automatic generation of schemes about
decidable equality, created by Vincent Siles, Oct 2007 *)
@@ -79,6 +77,25 @@ let sumbool = Coqlib.build_coq_sumbool
let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
+let induct_on c =
+ new_induct false
+ [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+ None (None,None) None
+
+let destruct_on_using c id =
+ new_destruct false
+ [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+ None
+ (None,Some (dl,Genarg.IntroOrAndPattern [
+ [dl,Genarg.IntroAnonymous];
+ [dl,Genarg.IntroIdentifier id]]))
+ None
+
+let destruct_on c =
+ new_destruct false
+ [Tacexpr.ElimOnConstr (Evd.empty,(c,Glob_term.NoBindings))]
+ None (None,None) None
+
(* reconstruct the inductive with the correct deBruijn indexes *)
let mkFullInd ind n =
let mib = Global.lookup_mind (fst ind) in
@@ -329,13 +346,12 @@ let do_replace_lb lb_scheme_key aavoid narg gls p q =
with Not_found ->
(* spiwack: the format of this error message should probably
be improved. *)
- let err_msg = msg_with Format.str_formatter
+ let err_msg = string_of_ppcmds
(str "Leibniz->boolean:" ++
str "You have to declare the" ++
str "decidability over " ++
Printer.pr_constr type_of_pq ++
- str " first.");
- Format.flush_str_formatter ()
+ str " first.")
in
error err_msg
in let lb_args = Array.append (Array.append
@@ -387,13 +403,12 @@ let do_replace_bl bl_scheme_key ind gls aavoid narg lft rgt =
with Not_found ->
(* spiwack: the format of this error message should probably
be improved. *)
- let err_msg = msg_with Format.str_formatter
+ let err_msg = string_of_ppcmds
(str "boolean->Leibniz:" ++
str "You have to declare the" ++
str "decidability over " ++
Printer.pr_constr tt1 ++
- str " first.");
- Format.flush_str_formatter ()
+ str " first.")
in
error err_msg
in let bl_args =
@@ -513,17 +528,9 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec gsig =
avoid := freshz::(!avoid);
tclTHENSEQ [ intros_using fresh_first_intros;
intro_using freshn ;
- new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
- Rawterm.NoBindings))]
- None
- (None,None)
- None;
+ induct_on (mkVar freshn);
intro_using freshm;
- new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm),
- Rawterm.NoBindings))]
- None
- (None,None)
- None;
+ destruct_on (mkVar freshm);
intro_using freshz;
intros;
tclTRY (
@@ -541,7 +548,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
in
avoid := fresht::(!avoid);
(new_destruct false [Tacexpr.ElimOnConstr
- ((mkVar freshz,Rawterm.NoBindings))]
+ (Evd.empty,((mkVar freshz,Glob_term.NoBindings)))]
None
(None, Some (dl,Genarg.IntroOrAndPattern [[
dl,Genarg.IntroIdentifier fresht;
@@ -551,7 +558,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- fun gls-> let gl = (gls.Evd.it).Evd.evar_concl in
+ fun gls-> let gl = pf_concl gls in
match (kind_of_term gl) with
| App (c,ca) -> (
match (kind_of_term c) with
@@ -583,7 +590,7 @@ let make_bl_scheme mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|Pfedit.build_by_tactic
+ [|Pfedit.build_by_tactic (Global.env())
(compute_bl_goal ind lnamesparrec nparrec)
(compute_bl_tact (!bl_scheme_kind_aux()) ind lnamesparrec nparrec)|]
@@ -651,30 +658,22 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec gsig =
avoid := freshz::(!avoid);
tclTHENSEQ [ intros_using fresh_first_intros;
intro_using freshn ;
- new_induct false [Tacexpr.ElimOnConstr
- ((mkVar freshn),Rawterm.NoBindings)]
- None
- (None,None)
- None;
+ induct_on (mkVar freshn);
intro_using freshm;
- new_destruct false [Tacexpr.ElimOnConstr
- ((mkVar freshm),Rawterm.NoBindings)]
- None
- (None,None)
- None;
+ destruct_on (mkVar freshm);
intro_using freshz;
intros;
tclTRY (
tclORELSE reflexivity (Equality.discr_tac false None)
);
- Equality.inj [] false (mkVar freshz,Rawterm.NoBindings);
+ Equality.inj [] false (mkVar freshz,Glob_term.NoBindings);
intros; simpl_in_concl;
Auto.default_auto;
tclREPEAT (
tclTHENSEQ [apply (andb_true_intro());
simplest_split ;Auto.default_auto ]
);
- fun gls -> let gl = (gls.Evd.it).Evd.evar_concl in
+ fun gls -> let gl = pf_concl gls in
(* assume the goal to be eq (eq_type ...) = true *)
match (kind_of_term gl) with
| App(c,ca) -> (match (kind_of_term ca.(1)) with
@@ -703,7 +702,7 @@ let make_lb_scheme mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|Pfedit.build_by_tactic
+ [|Pfedit.build_by_tactic (Global.env())
(compute_lb_goal ind lnamesparrec nparrec)
(compute_lb_tact (!lb_scheme_kind_aux()) ind lnamesparrec nparrec)|]
@@ -810,24 +809,11 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
assert_by (Name freshH) (
mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
)
- (tclTHEN
- (new_destruct false [Tacexpr.ElimOnConstr
- (eqbnm,Rawterm.NoBindings)]
- None
- (None,None)
- None)
- Auto.default_auto);
+ (tclTHEN (destruct_on eqbnm) Auto.default_auto);
(fun gsig ->
let freshH2 = fresh_id (!avoid) (id_of_string "H") gsig in
avoid := freshH2::(!avoid);
- tclTHENS (
- new_destruct false [Tacexpr.ElimOnConstr
- ((mkVar freshH),Rawterm.NoBindings)]
- None
- (None,Some (dl,Genarg.IntroOrAndPattern [
- [dl,Genarg.IntroAnonymous];
- [dl,Genarg.IntroIdentifier freshH2]])) None
- ) [
+ tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
(* left *)
tclTHENSEQ [
simplest_left;
@@ -850,10 +836,10 @@ let compute_dec_tact ind lnamesparrec nparrec gsig =
Auto.default_auto
]);
Equality.general_rewrite_bindings_in true
- all_occurrences false
+ all_occurrences true false
(List.hd !avoid)
((mkVar (List.hd (List.tl !avoid))),
- Rawterm.NoBindings
+ Glob_term.NoBindings
)
true;
Equality.discr_tac false None
@@ -870,7 +856,7 @@ let make_eq_decidability mind =
let nparrec = mib.mind_nparams_rec in
let lnonparrec,lnamesparrec =
context_chop (nparams-nparrec) mib.mind_params_ctxt in
- [|Pfedit.build_by_tactic
+ [|Pfedit.build_by_tactic (Global.env())
(compute_dec_goal ind lnamesparrec nparrec)
(compute_dec_tact ind lnamesparrec nparrec)|]
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 19:11:05 +0000