Imported Upstream version 8.3~rc1+dfsgupstream/8.3.rc1.dfsg

24 files changed, 25 insertions, 25 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index de2ba7c9..5f0f5e7d 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: clenvtac.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 72b812ce..3840cc0a 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: clenvtac.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index 91f0a9ff..24cf2c1d 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_expr.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Names
 open Util
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index d28d9a0d..8810820d 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: decl_mode.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index b6e77b43..b309c9f0 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_mode.mli 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Names
 open Term
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index a5a0cde4..484d5332 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: evar_refiner.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Util
 open Names
diff --git a/proofs/evar_refiner.mli b/proofs/evar_refiner.mli
index e4303f42..3f7f88d1 100644
--- a/proofs/evar_refiner.mli
+++ b/proofs/evar_refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: evar_refiner.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 83dc497c..fda14f53 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: logic.ml 13332 2010-07-26 22:12:43Z msozeau $ *)
 
 open Pp
 open Util
@@ -58,7 +58,7 @@ let rec catchable_exception = function
   (* unification errors *)
   | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
-		   |CannotFindWellTypedAbstraction _
+		   |CannotFindWellTypedAbstraction _|OccurCheck _
 		   |UnsolvableImplicit _)) -> true
   | Typeclasses_errors.TypeClassError
       (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
diff --git a/proofs/logic.mli b/proofs/logic.mli
index c7cf6472..960505ed 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: logic.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 3adfd522..171db848 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: pfedit.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index b5003425..1b284f8d 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: pfedit.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index b352fdc8..4c55af90 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: proof_trees.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Closure
 open Util
diff --git a/proofs/proof_trees.mli b/proofs/proof_trees.mli
index 477c3162..0a2c6e9a 100644
--- a/proofs/proof_trees.mli
+++ b/proofs/proof_trees.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: proof_trees.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Util
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index f7c937bd..d11e6676 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ *)
+(*i $Id: proof_type.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 (*i*)
 open Environ
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index c6f0658b..5f8a63b0 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: proof_type.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Environ
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index f7d83c0a..77a5db12 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: redexpr.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index 93c34d86..ce0cb8e7 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: redexpr.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Term
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index e0ed7861..ddb7eefc 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: refiner.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 2b213c3f..7126533d 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: refiner.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Term
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 8761bfae..00dfb122 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tacexpr.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Topconstr
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 60e79c19..55996f33 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: tacmach.ml 13323 2010-07-24 15:57:30Z herbelin $ *)
 
 open Pp
 open Util
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 489786ef..30851b95 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tacmach.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 (*i*)
 open Names
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 6455420c..75783ab4 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tactic_debug.ml 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Names
 open Constrextern
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 8a6a22c6..8f74eae6 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id$ i*)
+(*i $Id: tactic_debug.mli 13323 2010-07-24 15:57:30Z herbelin $ i*)
 
 open Environ
 open Pattern