summaryrefslogtreecommitdiff
path: root/plugins/firstorder
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
committerGravatar Stephane Glondu <steph@glondu.net>2011-12-25 13:19:42 +0100
commit300293c119981054c95182a90c829058530a6b6f (patch)
treed7303613741c5796b58ced7db24ec7203327dbb2 /plugins/firstorder
parent9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff)
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml4
-rw-r--r--plugins/firstorder/formula.mli4
-rw-r--r--plugins/firstorder/g_ground.ml44
-rw-r--r--plugins/firstorder/ground.ml4
-rw-r--r--plugins/firstorder/ground.mli4
-rw-r--r--plugins/firstorder/instances.ml4
-rw-r--r--plugins/firstorder/instances.mli4
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/firstorder/sequent.mli4
-rw-r--r--plugins/firstorder/unify.ml4
-rw-r--r--plugins/firstorder/unify.mli4
13 files changed, 26 insertions, 26 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index d039a930..1f3fd595 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: formula.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: formula.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Hipattern
open Names
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index fbb103c0..a831c087 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: formula.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: formula.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Names
diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4
index 19b63407..8e68506c 100644
--- a/plugins/firstorder/g_ground.ml4
+++ b/plugins/firstorder/g_ground.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -8,7 +8,7 @@
(*i camlp4deps: "parsing/grammar.cma" i*)
-(* $Id: g_ground.ml4 13344 2010-07-28 15:04:36Z msozeau $ *)
+(* $Id: g_ground.ml4 14641 2011-11-06 11:59:10Z herbelin $ *)
open Formula
open Sequent
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 354bcda2..163b9891 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ground.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ground.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Formula
open Sequent
diff --git a/plugins/firstorder/ground.mli b/plugins/firstorder/ground.mli
index ba8051da..8328bb3a 100644
--- a/plugins/firstorder/ground.mli
+++ b/plugins/firstorder/ground.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: ground.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: ground.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
val ground_tac: Tacmach.tactic ->
(Proof_type.goal Tacmach.sigma -> Sequent.t) -> Tacmach.tactic
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 714604ae..4802aaa3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: instances.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: instances.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Formula
open Sequent
diff --git a/plugins/firstorder/instances.mli b/plugins/firstorder/instances.mli
index 8b913719..537e40e7 100644
--- a/plugins/firstorder/instances.mli
+++ b/plugins/firstorder/instances.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: instances.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: instances.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Term
open Tacmach
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 9cff67dc..e6d73fb6 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: rules.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Util
open Names
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index ec6d2bd0..a5a6b614 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: rules.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: rules.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Tacmach
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1d439693..faac286e 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sequent.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: sequent.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Util
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index 1232f1e8..ef052605 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: sequent.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: sequent.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
open Util
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 835b0409..4e0ad108 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(*i $Id: unify.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: unify.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
open Util
open Formula
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index af2ce01d..4e0d88d3 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -1,12 +1,12 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: unify.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: unify.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
open Term
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 11:28:08 +0000