summaryrefslogtreecommitdiff
path: root/contrib/fourier
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/fourier')
-rw-r--r--contrib/fourier/Fourier.v2
-rw-r--r--contrib/fourier/Fourier_util.v2
-rw-r--r--contrib/fourier/fourier.ml2
-rw-r--r--contrib/fourier/fourierR.ml22
-rw-r--r--contrib/fourier/g_fourier.ml46
5 files changed, 17 insertions, 17 deletions
diff --git a/contrib/fourier/Fourier.v b/contrib/fourier/Fourier.v
index f6faf94c..8836b76e 100644
--- a/contrib/fourier/Fourier.v
+++ b/contrib/fourier/Fourier.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Fourier.v,v 1.4.2.1 2004/07/16 19:30:11 herbelin Exp $ *)
+(* $Id: Fourier.v 5920 2004-07-16 20:01:26Z herbelin $ *)
(* "Fourier's method to solve linear inequations/equations systems.".*)
diff --git a/contrib/fourier/Fourier_util.v b/contrib/fourier/Fourier_util.v
index abcd4449..c3257b7d 100644
--- a/contrib/fourier/Fourier_util.v
+++ b/contrib/fourier/Fourier_util.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: Fourier_util.v,v 1.4.2.1 2004/07/16 19:30:11 herbelin Exp $ *)
+(* $Id: Fourier_util.v 5920 2004-07-16 20:01:26Z herbelin $ *)
Require Export Rbase.
Comments "Lemmas used by the tactic Fourier".
diff --git a/contrib/fourier/fourier.ml b/contrib/fourier/fourier.ml
index f5763c34..ed804e94 100644
--- a/contrib/fourier/fourier.ml
+++ b/contrib/fourier/fourier.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: fourier.ml,v 1.2.16.1 2004/07/16 19:30:11 herbelin Exp $ *)
+(* $Id: fourier.ml 5920 2004-07-16 20:01:26Z herbelin $ *)
(* Méthode d'élimination de Fourier *)
(* Référence:
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml
index 49fa35da..f9518bcb 100644
--- a/contrib/fourier/fourierR.ml
+++ b/contrib/fourier/fourierR.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: fourierR.ml,v 1.14.2.2 2004/07/19 13:28:28 herbelin Exp $ *)
+(* $Id: fourierR.ml 7760 2005-12-30 10:49:13Z herbelin $ *)
@@ -76,7 +76,7 @@ open Vernacexpr
type ineq = Rlt | Rle | Rgt | Rge
let string_of_R_constant kn =
- match Names.repr_kn kn with
+ match Names.repr_con kn with
| MPfile dir, sec_dir, id when
sec_dir = empty_dirpath &&
string_of_dirpath dir = "Coq.Reals.Rdefinitions"
@@ -85,13 +85,13 @@ let string_of_R_constant kn =
let rec string_of_R_constr c =
match kind_of_term c with
- Cast (c,t) -> string_of_R_constr c
+ Cast (c,_,_) -> string_of_R_constr c
|Const c -> string_of_R_constant c
| _ -> "not_of_constant"
let rec rational_of_constr c =
match kind_of_term c with
- | Cast (c,t) -> (rational_of_constr c)
+ | Cast (c,_,_) -> (rational_of_constr c)
| App (c,args) ->
(match (string_of_R_constr c) with
| "Ropp" ->
@@ -122,7 +122,7 @@ let rec rational_of_constr c =
let rec flin_of_constr c =
try(
match kind_of_term c with
- | Cast (c,t) -> (flin_of_constr c)
+ | Cast (c,_,_) -> (flin_of_constr c)
| App (c,args) ->
(match (string_of_R_constr c) with
"Ropp" ->
@@ -221,7 +221,7 @@ let ineq1_of_constr (h,t) =
hstrict=false}]
|_->assert false)
| Ind (kn,i) ->
- if IndRef(kn,i) = Coqlib.glob_eqT then
+ if IndRef(kn,i) = Coqlib.glob_eq then
let t0= args.(0) in
let t1= args.(1) in
let t2= args.(2) in
@@ -281,7 +281,7 @@ let constant = Coqlib.gen_constant "Fourier"
(* Standard library *)
open Coqlib
-let coq_sym_eqT = lazy (build_coq_sym_eqT ())
+let coq_sym_eqT = lazy (build_coq_sym_eq ())
let coq_False = lazy (build_coq_False ())
let coq_not = lazy (build_coq_not ())
let coq_eq = lazy (build_coq_eq ())
@@ -303,7 +303,7 @@ let coq_R0 = lazy (constant_real "R0")
let coq_R1 = lazy (constant_real "R1")
(* RIneq *)
-let coq_Rinv_R1 = lazy (constant ["Reals";"RIneq"] "Rinv_R1")
+let coq_Rinv_1 = lazy (constant ["Reals";"RIneq"] "Rinv_1")
(* Fourier_util *)
let constant_fourier = constant ["fourier";"Fourier_util"]
@@ -408,7 +408,7 @@ let tac_zero_infeq_false gl (n,d) =
(tac_zero_inf_pos gl (-n,d)))
;;
-let create_meta () = mkMeta(new_meta());;
+let create_meta () = mkMeta(Evarutil.new_meta());;
let my_cut c gl=
let concl = pf_concl gl in
@@ -458,7 +458,7 @@ let mkAppL a =
(* Résolution d'inéquations linéaires dans R *)
let rec fourier gl=
- Library.check_required_library ["Coq";"fourier";"Fourier"];
+ 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,
@@ -604,7 +604,7 @@ let rec fourier gl=
(Ring.polynom [])
tclIDTAC;
(tclTHEN (apply (get coq_sym_eqT))
- (apply (get coq_Rinv_R1)))]
+ (apply (get coq_Rinv_1)))]
)
]));
diff --git a/contrib/fourier/g_fourier.ml4 b/contrib/fourier/g_fourier.ml4
index 05c3adbd..3a6be850 100644
--- a/contrib/fourier/g_fourier.ml4
+++ b/contrib/fourier/g_fourier.ml4
@@ -8,10 +8,10 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_fourier.ml4,v 1.1.12.1 2004/07/16 19:30:11 herbelin Exp $ *)
+(* $Id: g_fourier.ml4 7734 2005-12-26 14:06:51Z herbelin $ *)
open FourierR
-TACTIC EXTEND Fourier
- [ "FourierZ" (* constr_list(l) *) ] -> [ fourier (* l *) ]
+TACTIC EXTEND fourier
+ [ "fourierz" ] -> [ fourier ]
END
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-14 02:14:45 +0000