summaryrefslogtreecommitdiff
path: root/toplevel/auto_ind_decl.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2008-08-08 13:18:42 +0200
commit870075f34dd9fa5792bfbf413afd3b96f17e76a0 (patch)
tree0c647056de1832cf1dba5ba58758b9121418e4be /toplevel/auto_ind_decl.ml
parenta0cfa4f118023d35b767a999d5a2ac4b082857b4 (diff)
Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg
Diffstat (limited to 'toplevel/auto_ind_decl.ml')
-rw-r--r--toplevel/auto_ind_decl.ml30
1 files changed, 16 insertions, 14 deletions
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 094a77ff..49b9ce7a 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 11166 2008-06-22 13:23:35Z herbelin $ i*)
+(*i $Id: auto_ind_decl.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
open Tacmach
open Util
@@ -55,6 +55,8 @@ let subst_in_constr (_,subst,(ind,const)) =
exception EqNotFound of string
exception EqUnknown of string
+let dl = dummy_loc
+
(* Some pre declaration of constant we are going to use *)
let bb = constr_of_global Coqlib.glob_bool
@@ -514,13 +516,13 @@ let compute_bl_tact ind lnamesparrec nparrec =
new_induct false [ (Tacexpr.ElimOnConstr ((mkVar freshn),
Rawterm.NoBindings))]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshm;
new_destruct false [ (Tacexpr.ElimOnConstr ((mkVar freshm),
Rawterm.NoBindings))]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshz;
intros;
@@ -542,9 +544,9 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
(new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshz,Rawterm.NoBindings))]
None
- ( Genarg.IntroOrAndPattern [[
- Genarg.IntroIdentifier fresht;
- Genarg.IntroIdentifier freshz]]) None) gl
+ (None, Some (dl,Genarg.IntroOrAndPattern [[
+ dl,Genarg.IntroIdentifier fresht;
+ dl,Genarg.IntroIdentifier freshz]])) None) gl
]);
(*
Ci a1 ... an = Ci b1 ... bn
@@ -632,13 +634,13 @@ let compute_lb_tact ind lnamesparrec nparrec =
new_induct false [Tacexpr.ElimOnConstr
((mkVar freshn),Rawterm.NoBindings)]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshm;
new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshm),Rawterm.NoBindings)]
None
- Genarg.IntroAnonymous
+ (None,None)
None;
intro_using freshz;
intros;
@@ -746,7 +748,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
Pfedit.by ( tclTHENSEQ [
intros_using fresh_first_intros;
intros_using [freshn;freshm];
- assert_as true (Genarg.IntroIdentifier freshH) (
+ assert_as true (dl,Genarg.IntroIdentifier freshH) (
mkApp(sumbool(),[|eqtrue eqbnm; eqfalse eqbnm|])
) ]);
(*we do this so we don't have to prove the same goal twice *)
@@ -754,7 +756,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
(new_destruct false [Tacexpr.ElimOnConstr
(eqbnm,Rawterm.NoBindings)]
None
- Genarg.IntroAnonymous
+ (None,None)
None)
Auto.default_auto
);
@@ -764,9 +766,9 @@ let compute_dec_tact ind lnamesparrec nparrec =
new_destruct false [Tacexpr.ElimOnConstr
((mkVar freshH),Rawterm.NoBindings)]
None
- (Genarg.IntroOrAndPattern [
- [Genarg.IntroAnonymous];
- [Genarg.IntroIdentifier freshH2]]) None
+ (None,Some (dl,Genarg.IntroOrAndPattern [
+ [dl,Genarg.IntroAnonymous];
+ [dl,Genarg.IntroIdentifier freshH2]])) None
);
let arfresh = Array.of_list fresh_first_intros in
let xargs = Array.sub arfresh 0 (2*nparrec) in
@@ -793,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 (Genarg.IntroIdentifier freshH3)
+ assert_as true (dl,Genarg.IntroIdentifier freshH3)
(mkApp(eq,[|bb;mkApp(eqI,[|mkVar freshm;mkVar freshm|]);tt|]))
]);
Pfedit.by