summaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2009-02-01 00:54:40 +0100
commitcfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch)
treeb7832bd5d412a5a5d69cb36ae2ded62c71124c22 /toplevel/auto_ind_decl.ml
parent113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff)
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
-rw-r--r--toplevel/auto_ind_decl.ml12
1 files changed, 6 insertions, 6 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 49b9ce7a..82709db4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: auto_ind_decl.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: auto_ind_decl.ml 11671 2008-12-12 12:43:03Z herbelin $ i*)
open Tacmach
open Util
@@ -530,13 +530,13 @@ let compute_bl_tact ind lnamesparrec nparrec =
tclORELSE reflexivity (Equality.discr_tac false None)
);
simpl_in_hyp
- ((Rawterm.all_occurrences_expr,freshz),Tacexpr.InHyp);
+ ((Rawterm.all_occurrences_expr,freshz),InHyp);
(*
repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
*)
tclREPEAT (
tclTHENSEQ [
- apply_in false freshz [(andb_prop()),Rawterm.NoBindings];
+ apply_in false false freshz [(Evd.empty,andb_prop()),Rawterm.NoBindings] None;
fun gl ->
let fresht = fresh_id (!avoid) (id_of_string "Z") gsig
in
@@ -748,8 +748,8 @@ let compute_dec_tact ind lnamesparrec nparrec =
Pfedit.by ( tclTHENSEQ [
intros_using fresh_first_intros;
intros_using [freshn;freshm];
- assert_as true (dl,Genarg.IntroIdentifier freshH) (
- mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
+ assert_tac (Name freshH) (
+ mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
) ]);
(*we do this so we don't have to prove the same goal twice *)
Pfedit.by ( tclTHEN
@@ -795,7 +795,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
unfold_constr (Lazy.force Coqlib.coq_not_ref);
intro;
Equality.subst_all;
- assert_as true (dl,Genarg.IntroIdentifier freshH3)
+ assert_tac (Name freshH3)
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
]);
Pfedit.by