diff options
Diffstat (limited to 'plugins/fourier')
| -rw-r--r-- | plugins/fourier/fourierR.ml | 17 |
1 files changed, 9 insertions, 8 deletions
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml index aeb07fc3a..d34d50364 100644 --- a/plugins/fourier/fourierR.ml +++ b/plugins/fourier/fourierR.ml @@ -87,7 +87,7 @@ let string_of_R_constant kn = 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 @@ -114,7 +114,7 @@ let rec rational_of_constr c = rminus (rational_of_constr args.(0)) (rational_of_constr args.(1)) | _ -> raise NoRational) - | Const kn -> + | Const (kn,_) -> (match (string_of_R_constant kn) with "R1" -> r1 |"R0" -> r0 @@ -160,7 +160,7 @@ let rec flin_of_constr c = with NoRational -> flin_add (flin_zero()) args.(0) (rinv b)) |_-> raise NoLinear) - | Const c -> + | Const (c,_) -> (match (string_of_R_constant c) with "R1" -> flin_one () |"R0" -> flin_zero () @@ -194,7 +194,7 @@ 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 -> + | Const (c,_) when Array.length args = 2 -> let t1= args.(0) in let t2= args.(1) in (match (string_of_R_constant c) with @@ -227,13 +227,13 @@ let ineq1_of_constr (h,t) = (flin_of_constr t1); hstrict=false}] |_-> raise NoIneq) - | Ind (kn,i) -> + | 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 -> + | Const (c,_) -> (match (string_of_R_constant c) with | "R"-> [{hname=h; @@ -609,8 +609,9 @@ let rec fourier gl= [tclORELSE (* TODO : Ring.polynom []*) tclIDTAC tclIDTAC; - (tclTHEN (apply (get coq_sym_eqT)) - (apply (get coq_Rinv_1)))] + pf_constr_of_global (get coq_sym_eqT) (fun symeq -> + (tclTHEN (apply symeq) + (apply (get coq_Rinv_1))))] ) ])); |