summaryrefslogtreecommitdiff
path: root/plugins/fourier/fourierR.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/fourier/fourierR.ml')
-rw-r--r--plugins/fourier/fourierR.ml321
1 files changed, 160 insertions, 161 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 763383dd..8006a3e1 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,25 +8,24 @@
-(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
-des inéquations et équations sont entiers. En attendant la tactique Field.
+(* La tactique Fourier ne fonctionne de manière sûre que si les coefficients
+des inéquations et équations sont entiers. En attendant la tactique Field.
*)
open Term
open Tactics
-open Clenv
open Names
-open Libnames
+open Globnames
open Tacticals
open Tacmach
open Fourier
open Contradiction
(******************************************************************************
-Opérations sur les combinaisons linéaires affines.
-La partie homogène d'une combinaison linéaire est en fait une table de hash
+Opérations sur les combinaisons linéaires affines.
+La partie homogène d'une combinaison linéaire est en fait une table de hash
qui donne le coefficient d'un terme du calcul des constructions,
-qui est zéro si le terme n'y est pas.
+qui est zéro si le terme n'y est pas.
*)
module Constrhash = Hashtbl.Make
@@ -40,12 +39,11 @@ type flin = {fhom: rational Constrhash.t;
let flin_zero () = {fhom=Constrhash.create 50;fcste=r0};;
-let flin_coef f x = try (Constrhash.find f.fhom x) with Not_found -> r0;;
+let flin_coef f x = try Constrhash.find f.fhom x with Not_found -> r0;;
let flin_add f x c =
let cx = flin_coef f x in
- Constrhash.remove f.fhom x;
- Constrhash.add f.fhom x (rplus cx c);
+ Constrhash.replace f.fhom x (rplus cx c);
f
;;
let flin_add_cste f c =
@@ -75,24 +73,25 @@ let flin_emult a f =
;;
(*****************************************************************************)
-open Vernacexpr
type ineq = Rlt | Rle | Rgt | Rge
let string_of_R_constant kn =
match Names.repr_con kn with
| MPfile dir, sec_dir, id when
- sec_dir = empty_dirpath &&
- string_of_dirpath dir = "Coq.Reals.Rdefinitions"
- -> string_of_label id
+ sec_dir = DirPath.empty &&
+ DirPath.to_string dir = "Coq.Reals.Rdefinitions"
+ -> Label.to_string id
| _ -> "constant_not_of_R"
let rec string_of_R_constr c =
match kind_of_term c with
Cast (c,_,_) -> string_of_R_constr c
- |Const c -> string_of_R_constant c
+ |Const (c,_) -> string_of_R_constant c
| _ -> "not_of_constant"
+exception NoRational
+
let rec rational_of_constr c =
match kind_of_term c with
| Cast (c,_,_) -> (rational_of_constr c)
@@ -114,15 +113,17 @@ let rec rational_of_constr c =
| "Rminus" ->
rminus (rational_of_constr args.(0))
(rational_of_constr args.(1))
- | _ -> failwith "not a rational")
- | Const kn ->
+ | _ -> raise NoRational)
+ | Const (kn,_) ->
(match (string_of_R_constant kn) with
"R1" -> r1
|"R0" -> r0
- | _ -> failwith "not a rational")
- | _ -> failwith "not a rational"
+ | _ -> raise NoRational)
+ | _ -> raise NoRational
;;
+exception NoLinear
+
let rec flin_of_constr c =
try(
match kind_of_term c with
@@ -138,39 +139,34 @@ let rec flin_of_constr c =
flin_minus (flin_of_constr args.(0))
(flin_of_constr args.(1))
| "Rmult"->
- (try (let a=(rational_of_constr args.(0)) in
- try (let b = (rational_of_constr args.(1)) in
- (flin_add_cste (flin_zero()) (rmult a b)))
- with e when Errors.noncritical e ->
- (flin_add (flin_zero())
- args.(1)
- a))
- with e when Errors.noncritical e ->
- (flin_add (flin_zero())
- args.(0)
- (rational_of_constr args.(1))))
+ (try
+ let a = rational_of_constr args.(0) in
+ try
+ let b = rational_of_constr args.(1) in
+ flin_add_cste (flin_zero()) (rmult a b)
+ with NoRational ->
+ flin_add (flin_zero()) args.(1) a
+ with NoRational ->
+ flin_add (flin_zero()) args.(0)
+ (rational_of_constr args.(1)))
| "Rinv"->
- let a=(rational_of_constr args.(0)) in
- flin_add_cste (flin_zero()) (rinv a)
+ let a = rational_of_constr args.(0) in
+ flin_add_cste (flin_zero()) (rinv a)
| "Rdiv"->
- (let b=(rational_of_constr args.(1)) in
- try (let a = (rational_of_constr args.(0)) in
- (flin_add_cste (flin_zero()) (rdiv a b)))
- with e when Errors.noncritical e ->
- (flin_add (flin_zero())
- args.(0)
- (rinv b)))
- |_->assert false)
- | Const c ->
+ (let b = rational_of_constr args.(1) in
+ try
+ let a = rational_of_constr args.(0) in
+ flin_add_cste (flin_zero()) (rdiv a b)
+ with NoRational ->
+ flin_add (flin_zero()) args.(0) (rinv b))
+ |_-> raise NoLinear)
+ | Const (c,_) ->
(match (string_of_R_constant c) with
"R1" -> flin_one ()
|"R0" -> flin_zero ()
- |_-> assert false)
- |_-> assert false)
- with e when Errors.noncritical e ->
- flin_add (flin_zero())
- c
- r1
+ |_-> raise NoLinear)
+ |_-> raise NoLinear)
+ with NoRational | NoLinear -> flin_add (flin_zero()) c r1
;;
let flin_to_alist f =
@@ -179,9 +175,9 @@ let flin_to_alist f =
!res
;;
-(* Représentation des hypothèses qui sont des inéquations ou des équations.
+(* Représentation des hypothèses qui sont des inéquations ou des équations.
*)
-type hineq={hname:constr; (* le nom de l'hypothèse *)
+type hineq={hname:constr; (* le nom de l'hypothèse *)
htype:string; (* Rlt, Rgt, Rle, Rge, eqTLR ou eqTRL *)
hleft:constr;
hright:constr;
@@ -189,54 +185,57 @@ type hineq={hname:constr; (* le nom de l'hypothèse *)
hstrict:bool}
;;
-(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
+(* Transforme une hypothese h:t en inéquation flin<0 ou flin<=0
*)
+
+exception NoIneq
+
let ineq1_of_constr (h,t) =
match (kind_of_term t) with
- App (f,args) ->
- (match kind_of_term f with
- Const c when Array.length args = 2 ->
- let t1= args.(0) in
- let t2= args.(1) in
+ | App (f,args) ->
+ (match kind_of_term f with
+ | Const (c,_) when Array.length args = 2 ->
+ let t1= args.(0) in
+ let t2= args.(1) in
(match (string_of_R_constant c) with
- "Rlt" -> [{hname=h;
+ |"Rlt" -> [{hname=h;
htype="Rlt";
hleft=t1;
hright=t2;
hflin= flin_minus (flin_of_constr t1)
(flin_of_constr t2);
hstrict=true}]
- |"Rgt" -> [{hname=h;
+ |"Rgt" -> [{hname=h;
htype="Rgt";
hleft=t2;
hright=t1;
hflin= flin_minus (flin_of_constr t2)
(flin_of_constr t1);
hstrict=true}]
- |"Rle" -> [{hname=h;
+ |"Rle" -> [{hname=h;
htype="Rle";
hleft=t1;
hright=t2;
hflin= flin_minus (flin_of_constr t1)
(flin_of_constr t2);
hstrict=false}]
- |"Rge" -> [{hname=h;
+ |"Rge" -> [{hname=h;
htype="Rge";
hleft=t2;
hright=t1;
hflin= flin_minus (flin_of_constr t2)
(flin_of_constr t1);
hstrict=false}]
- |_->assert false)
- | Ind (kn,i) ->
- if IndRef(kn,i) = Coqlib.glob_eq then
- let t0= args.(0) in
- let t1= args.(1) in
- let t2= args.(2) in
- (match (kind_of_term t0) with
- Const c ->
- (match (string_of_R_constant c) with
- "R"->
+ |_-> raise NoIneq)
+ | Ind ((kn,i),_) ->
+ if not (eq_gr (IndRef(kn,i)) Coqlib.glob_eq) then raise NoIneq;
+ let t0= args.(0) in
+ let t1= args.(1) in
+ let t2= args.(2) in
+ (match (kind_of_term t0) with
+ | Const (c,_) ->
+ (match (string_of_R_constant c) with
+ | "R"->
[{hname=h;
htype="eqTLR";
hleft=t1;
@@ -251,20 +250,18 @@ let ineq1_of_constr (h,t) =
hflin= flin_minus (flin_of_constr t2)
(flin_of_constr t1);
hstrict=false}]
- |_-> assert false)
- |_-> assert false)
- else
- assert false
- |_-> assert false)
- |_-> assert false
+ |_-> raise NoIneq)
+ |_-> raise NoIneq)
+ |_-> raise NoIneq)
+ |_-> raise NoIneq
;;
-(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
+(* Applique la méthode de Fourier à une liste d'hypothèses (type hineq)
*)
let fourier_lineq lineq1 =
let nvar=ref (-1) in
- let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
+ let hvar=Constrhash.create 50 in (* la table des variables des inéquations *)
List.iter (fun f ->
Constrhash.iter (fun x _ -> if not (Constrhash.mem hvar x) then begin
nvar:=(!nvar)+1;
@@ -273,7 +270,7 @@ let fourier_lineq lineq1 =
f.hflin.fhom)
lineq1;
let sys= List.map (fun h->
- let v=Array.create ((!nvar)+1) r0 in
+ let v=Array.make ((!nvar)+1) r0 in
Constrhash.iter (fun x c -> v.(Constrhash.find hvar x)<-c)
h.hflin.fhom;
((Array.to_list v)@[rop h.hflin.fcste],h.hstrict))
@@ -345,14 +342,14 @@ let coq_Rnot_le_le = lazy (constant_fourier "Rnot_le_le")
let coq_Rlt_not_le_frac_opp = lazy (constant_fourier "Rlt_not_le_frac_opp")
(******************************************************************************
-Construction de la preuve en cas de succès de la méthode de Fourier,
+Construction de la preuve en cas de succès de la méthode de Fourier,
i.e. on obtient une contradiction.
*)
let is_int x = (x.den)=1
;;
(* fraction = couple (num,den) *)
-let rec rational_to_fraction x= (x.num,x.den)
+let rational_to_fraction x= (x.num,x.den)
;;
(* traduction -3 -> (Ropp (Rplus R1 (Rplus R1 R1)))
@@ -363,7 +360,7 @@ let int_to_real n =
then get coq_R0
else
(let s=ref (get coq_R1) in
- for i=1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done;
+ for _i = 1 to (nn-1) do s:=mkApp (get coq_Rplus,[|get coq_R1;!s|]) done;
if n<0 then mkApp (get coq_Ropp, [|!s|]) else !s)
;;
(* -1/2 -> (Rmult (Ropp R1) (Rinv (Rplus R1 R1)))
@@ -379,11 +376,11 @@ let rational_to_real x =
let tac_zero_inf_pos gl (n,d) =
let tacn=ref (apply (get coq_Rlt_zero_1)) in
let tacd=ref (apply (get coq_Rlt_zero_1)) in
- for i=1 to n-1 do
- tacn:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
- for i=1 to d-1 do
- tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
- (tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
+ for _i = 1 to n - 1 do
+ tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacn); done;
+ for _i = 1 to d - 1 do
+ tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
+ (Tacticals.New.tclTHENS (apply (get coq_Rlt_mult_inv_pos)) [!tacn;!tacd])
;;
(* preuve que 0<=n*1/d
@@ -393,11 +390,11 @@ let tac_zero_infeq_pos gl (n,d)=
then (apply (get coq_Rle_zero_zero))
else (apply (get coq_Rle_zero_1))) in
let tacd=ref (apply (get coq_Rlt_zero_1)) in
- for i=1 to n-1 do
- tacn:=(tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
- for i=1 to d-1 do
- tacd:=(tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
- (tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
+ for _i = 1 to n - 1 do
+ tacn:=(Tacticals.New.tclTHEN (apply (get coq_Rle_zero_pos_plus1)) !tacn); done;
+ for _i = 1 to d - 1 do
+ tacd:=(Tacticals.New.tclTHEN (apply (get coq_Rlt_zero_pos_plus1)) !tacd); done;
+ (Tacticals.New.tclTHENS (apply (get coq_Rle_mult_inv_pos)) [!tacn;!tacd])
;;
(* preuve que 0<(-n)*(1/d) => False
@@ -405,14 +402,14 @@ let tac_zero_infeq_pos gl (n,d)=
let tac_zero_inf_false gl (n,d) =
if n=0 then (apply (get coq_Rnot_lt0))
else
- (tclTHEN (apply (get coq_Rle_not_lt))
+ (Tacticals.New.tclTHEN (apply (get coq_Rle_not_lt))
(tac_zero_infeq_pos gl (-n,d)))
;;
(* preuve que 0<=(-n)*(1/d) => False
*)
let tac_zero_infeq_false gl (n,d) =
- (tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
+ (Tacticals.New.tclTHEN (apply (get coq_Rlt_not_le_frac_opp))
(tac_zero_inf_pos gl (-n,d)))
;;
@@ -425,18 +422,16 @@ let my_cut c gl=
let exact = exact_check;;
-let tac_use h = match h.htype with
- "Rlt" -> exact h.hname
- |"Rle" -> exact h.hname
- |"Rgt" -> (tclTHEN (apply (get coq_Rfourier_gt_to_lt))
- (exact h.hname))
- |"Rge" -> (tclTHEN (apply (get coq_Rfourier_ge_to_le))
- (exact h.hname))
- |"eqTLR" -> (tclTHEN (apply (get coq_Rfourier_eqLR_to_le))
- (exact h.hname))
- |"eqTRL" -> (tclTHEN (apply (get coq_Rfourier_eqRL_to_le))
- (exact h.hname))
- |_->assert false
+let tac_use h =
+ let tac = exact h.hname in
+ match h.htype with
+ "Rlt" -> tac
+ |"Rle" -> tac
+ |"Rgt" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_gt_to_lt)) tac)
+ |"Rge" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_ge_to_le)) tac)
+ |"eqTLR" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqLR_to_le)) tac)
+ |"eqTRL" -> (Tacticals.New.tclTHEN (apply (get coq_Rfourier_eqRL_to_le)) tac)
+ |_->assert false
;;
(*
@@ -464,58 +459,61 @@ let mkAppL a =
mkApp(List.hd l, Array.of_list (List.tl l))
;;
-(* Résolution d'inéquations linéaires dans R *)
-let rec fourier gl=
+exception GoalDone
+
+(* Résolution d'inéquations linéaires dans R *)
+let rec fourier () =
+ Proofview.Goal.nf_enter begin fun gl ->
+ let concl = Proofview.Goal.concl gl in
Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
- let goal = strip_outer_cast (pf_concl gl) in
- let fhyp=id_of_string "new_hyp_for_fourier" in
- (* si le but est une inéquation, on introduit son contraire,
- et le but à prouver devient False *)
- try (let tac =
- match (kind_of_term goal) with
+ let goal = strip_outer_cast concl in
+ let fhyp=Id.of_string "new_hyp_for_fourier" in
+ (* si le but est une inéquation, on introduit son contraire,
+ et le but à prouver devient False *)
+ try
+ match (kind_of_term goal) with
App (f,args) ->
(match (string_of_R_constr f) with
"Rlt" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_ge_lt))
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_ge_lt))
(intro_using fhyp))
- fourier)
+ (fourier ()))
|"Rle" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_gt_le))
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_gt_le))
(intro_using fhyp))
- fourier)
+ (fourier ()))
|"Rgt" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_le_gt))
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_le_gt))
(intro_using fhyp))
- fourier)
+ (fourier ()))
|"Rge" ->
- (tclTHEN
- (tclTHEN (apply (get coq_Rfourier_not_lt_ge))
+ (Tacticals.New.tclTHEN
+ (Tacticals.New.tclTHEN (apply (get coq_Rfourier_not_lt_ge))
(intro_using fhyp))
- fourier)
- |_->assert false)
- |_->assert false
- in tac gl)
- with e when Errors.noncritical e ->
- (* les hypothèses *)
+ (fourier ()))
+ |_-> raise GoalDone)
+ |_-> raise GoalDone
+ with GoalDone ->
+ (* les hypothèses *)
let hyps = List.map (fun (h,t)-> (mkVar h,t))
- (list_of_sign (pf_hyps gl)) in
+ (list_of_sign (Proofview.Goal.hyps gl)) in
let lineq =ref [] in
List.iter (fun h -> try (lineq:=(ineq1_of_constr h)@(!lineq))
- with e when Errors.noncritical e -> ())
+ with NoIneq -> ())
hyps;
- (* lineq = les inéquations découlant des hypothèses *)
- if !lineq=[] then Util.error "No inequalities";
+ (* lineq = les inéquations découlant des hypothèses *)
+ if !lineq=[] then Errors.error "No inequalities";
let res=fourier_lineq (!lineq) in
- let tac=ref tclIDTAC in
+ let tac=ref (Proofview.tclUNIT ()) in
if res=[]
- then Util.error "fourier failed"
- (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
+ then Errors.error "fourier failed"
+ (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *)
else (match res with
[(cres,sres,lc)]->
- (* lc=coefficients multiplicateurs des inéquations
+ (* lc=coefficients multiplicateurs des inéquations
qui donnent 0<cres ou 0<=cres selon sres *)
(*print_string "Fourier's method can prove the goal...";flush stdout;*)
let lutil=ref [] in
@@ -525,7 +523,7 @@ let rec fourier gl=
then (lutil:=(h,c)::(!lutil)(*;
print_rational(c);print_string " "*)))
(List.combine (!lineq) lc);
- (* on construit la combinaison linéaire des inéquation *)
+ (* on construit la combinaison linéaire des inéquation *)
(match (!lutil) with
(h1,c1)::lutil ->
let s=ref (h1.hstrict) in
@@ -554,11 +552,11 @@ let rec fourier gl=
let tc=rational_to_real cres in
(* puis sa preuve *)
let tac1=ref (if h1.hstrict
- then (tclTHENS (apply (get coq_Rfourier_lt))
+ then (Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt))
[tac_use h1;
tac_zero_inf_pos gl
(rational_to_fraction c1)])
- else (tclTHENS (apply (get coq_Rfourier_le))
+ else (Tacticals.New.tclTHENS (apply (get coq_Rfourier_le))
[tac_use h1;
tac_zero_inf_pos gl
(rational_to_fraction c1)])) in
@@ -566,20 +564,20 @@ let rec fourier gl=
List.iter (fun (h,c)->
(if (!s)
then (if h.hstrict
- then tac1:=(tclTHENS (apply (get coq_Rfourier_lt_lt))
+ then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_lt))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (get coq_Rfourier_lt_le))
+ else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_lt_le))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)]))
else (if h.hstrict
- then tac1:=(tclTHENS (apply (get coq_Rfourier_le_lt))
+ then tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_lt))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)])
- else tac1:=(tclTHENS (apply (get coq_Rfourier_le_le))
+ else tac1:=(Tacticals.New.tclTHENS (apply (get coq_Rfourier_le_le))
[!tac1;tac_use h;
tac_zero_inf_pos gl
(rational_to_fraction c)])));
@@ -589,42 +587,43 @@ let rec fourier gl=
then tac_zero_inf_false gl (rational_to_fraction cres)
else tac_zero_infeq_false gl (rational_to_fraction cres)
in
- tac:=(tclTHENS (my_cut ineq)
- [tclTHEN (change_in_concl None
+ tac:=(Tacticals.New.tclTHENS (Proofview.V82.tactic (my_cut ineq))
+ [Tacticals.New.tclTHEN (change_concl
(mkAppL [| get coq_not; ineq|]
))
- (tclTHEN (apply (if sres then get coq_Rnot_lt_lt
+ (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
else get coq_Rnot_le_le))
- (tclTHENS (Equality.replace
+ (Tacticals.New.tclTHENS (Equality.replace
(mkAppL [|get coq_Rminus;!t2;!t1|]
)
tc)
[tac2;
- (tclTHENS
+ (Tacticals.New.tclTHENS
(Equality.replace
(mkApp (get coq_Rinv,
[|get coq_R1|]))
(get coq_R1))
-(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
+(* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
- [tclORELSE
- (Ring.polynom [])
- tclIDTAC;
- (tclTHEN (apply (get coq_sym_eqT))
- (apply (get coq_Rinv_1)))]
+ [Tacticals.New.tclORELSE
+ (* TODO : Ring.polynom []*) (Proofview.tclUNIT ())
+ (Proofview.tclUNIT ());
+ Tacticals.New.pf_constr_of_global (get coq_sym_eqT) (fun symeq ->
+ (Tacticals.New.tclTHEN (apply symeq)
+ (apply (get coq_Rinv_1))))]
)
]));
!tac1]);
- tac:=(tclTHENS (cut (get coq_False))
- [tclTHEN intro (contradiction None);
+ tac:=(Tacticals.New.tclTHENS (cut (get coq_False))
+ [Tacticals.New.tclTHEN intro (contradiction None);
!tac])
|_-> assert false) |_-> assert false
);
(* ((tclTHEN !tac (tclFAIL 1 (* 1 au hasard... *))) gl) *)
- (!tac gl)
+ !tac
(* ((tclABSTRACT None !tac) gl) *)
-
+ end
;;
(*
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-14 16:42:21 +0000