summaryrefslogtreecommitdiff
path: root/plugins/fourier
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/fourier')
-rw-r--r--plugins/fourier/Fourier.v2
-rw-r--r--plugins/fourier/Fourier_util.v2
-rw-r--r--plugins/fourier/fourier.ml2
-rw-r--r--plugins/fourier/fourierR.ml2
-rw-r--r--plugins/fourier/g_fourier.ml42
5 files changed, 5 insertions, 5 deletions
diff --git a/plugins/fourier/Fourier.v b/plugins/fourier/Fourier.v
index 2304ddbe..05e85cde 100644
--- a/plugins/fourier/Fourier.v
+++ b/plugins/fourier/Fourier.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Fourier.v 13323 2010-07-24 15:57:30Z herbelin $ *)
(* "Fourier's method to solve linear inequations/equations systems.".*)
diff --git a/plugins/fourier/Fourier_util.v b/plugins/fourier/Fourier_util.v
index 152bbc04..3cd26cb8 100644
--- a/plugins/fourier/Fourier_util.v
+++ b/plugins/fourier/Fourier_util.v
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: Fourier_util.v 13323 2010-07-24 15:57:30Z herbelin $ *)
Require Export Rbase.
Comments "Lemmas used by the tactic Fourier".
diff --git a/plugins/fourier/fourier.ml b/plugins/fourier/fourier.ml
index 081246da..16123fd7 100644
--- a/plugins/fourier/fourier.ml
+++ b/plugins/fourier/fourier.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: fourier.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
(* Méthode d'élimination de Fourier *)
(* Référence:
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index 0af2849e..e9392e78 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id$ *)
+(* $Id: fourierR.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
diff --git a/plugins/fourier/g_fourier.ml4 b/plugins/fourier/g_fourier.ml4
index c6976ff7..d3b8228d 100644
--- a/plugins/fourier/g_fourier.ml4
+++ b/plugins/fourier/g_fourier.ml4
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id$ *)
+(* $Id: g_fourier.ml4 13323 2010-07-24 15:57:30Z herbelin $ *)
open FourierR