diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-25 13:19:49 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-25 13:19:49 +0000 |
| commit | 4eca8cad5398288761e242e91339427bf2610847 (patch) | |
| tree | afeb00e715959f5250f567c70e18323f078a2702 /contrib/fourier | |
| parent | f3c6e557b2a8d53fefe7398294098028e33c9b09 (diff) | |
Traduction des noms v7 de R en noms v8
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7725 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/fourier')
| -rw-r--r-- | contrib/fourier/fourierR.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index e40cd2676..8a546f90f 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -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"] @@ -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)))] ) ])); |