diff options
author | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
---|---|---|
committer | Samuel Mimram <smimram@debian.org> | 2006-04-28 14:59:16 +0000 |
commit | 3ef7797ef6fc605dfafb32523261fe1b023aeecb (patch) | |
tree | ad89c6bb57ceee608fcba2bb3435b74e0f57919e /contrib/fourier | |
parent | 018ee3b0c2be79eb81b1f65c3f3fa142d24129c8 (diff) |
Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha
Diffstat (limited to 'contrib/fourier')
-rw-r--r-- | contrib/fourier/Fourier.v | 2 | ||||
-rw-r--r-- | contrib/fourier/Fourier_util.v | 2 | ||||
-rw-r--r-- | contrib/fourier/fourier.ml | 2 | ||||
-rw-r--r-- | contrib/fourier/fourierR.ml | 22 | ||||
-rw-r--r-- | contrib/fourier/g_fourier.ml4 | 6 |
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 |