Imported Upstream version 8.3.pl3upstream/8.3.pl3

24 files changed, 50 insertions, 49 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 5f0f5e7d..7b760859 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.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: clenvtac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: clenvtac.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 3840cc0a..45e12645 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.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: clenvtac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: clenvtac.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index 24cf2c1d..5c069cdd 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.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: decl_expr.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: decl_expr.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Names
 open Util
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index 8810820d..250c1655 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.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: decl_mode.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: decl_mode.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index b309c9f0..60cb99c1 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.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: decl_mode.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: decl_mode.mli 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Names
 open Term
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 484d5332..69168dbd 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.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: evar_refiner.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: evar_refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Util
 open Names
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index 3f7f88d1..69d4853e 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.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: evar_refiner.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: evar_refiner.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/proofs/logic.ml b/proofs/logic.ml
index fda14f53..d837dca5 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.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: logic.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
+(* $Id: logic.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
@@ -323,7 +323,8 @@ let check_conv_leq_goal env sigma arg ty conclty =
     raise (RefinerError (BadType (arg,ty,conclty)))
 
 let goal_type_of env sigma c =
-  (if !check then type_of else Retyping.get_type_of ~refresh:true) env sigma c
+  if !check then type_of env sigma c
+  else Retyping.get_type_of ~refresh:true env sigma c
 
 let rec mk_refgoals sigma goal goalacc conclty trm =
   let env = evar_env goal in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 960505ed..da2566a7 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.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: logic.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: logic.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 42111213..a9799f38 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.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: pfedit.ml 13981 2011-04-08 16:59:26Z herbelin $ *)
+(* $Id: pfedit.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 8df26706..05c329c1 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.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: pfedit.mli 13981 2011-04-08 16:59:26Z herbelin $ i*)
+(*i $Id: pfedit.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 4c55af90..8fe1a4c2 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.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: proof_trees.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: proof_trees.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Closure
 open Util
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 0a2c6e9a..9e9f5e63 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.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: proof_trees.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: proof_trees.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index d11e6676..46fce6ae 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.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: proof_type.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(*i $Id: proof_type.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 (*i*)
 open Environ
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 5f8a63b0..417f75da 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.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: proof_type.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: proof_type.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Environ
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 77a5db12..7290a92f 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.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: redexpr.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: redexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index ce0cb8e7..9eaa91cc 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.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: redexpr.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: redexpr.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index ddb7eefc..a540eef6 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.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: refiner.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: refiner.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 7126533d..8167bfb2 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.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: refiner.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: refiner.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 00dfb122..563d073a 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.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: tacexpr.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: tacexpr.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Topconstr
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 55996f33..3939a78b 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.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: tacmach.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
+(* $Id: tacmach.ml 14641 2011-11-06 11:59:10Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 30851b95..6938c320 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.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: tacmach.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: tacmach.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 75783ab4..7922eeb0 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.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: tactic_debug.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: tactic_debug.ml 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Names
 open Constrextern
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 8f74eae6..e2606a06 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.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: tactic_debug.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
+(*i $Id: tactic_debug.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
 
 open Environ
 open Pattern