From f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Fri, 6 Aug 2010 16:15:08 -0400 Subject: Imported Upstream version 8.3~rc1+dfsg --- proofs/clenvtac.ml | 2 +- proofs/clenvtac.mli | 2 +- proofs/decl_expr.mli | 2 +- proofs/decl_mode.ml | 2 +- proofs/decl_mode.mli | 2 +- proofs/evar_refiner.ml | 2 +- proofs/evar_refiner.mli | 2 +- proofs/logic.ml | 4 ++-- proofs/logic.mli | 2 +- proofs/pfedit.ml | 2 +- proofs/pfedit.mli | 2 +- proofs/proof_trees.ml | 2 +- proofs/proof_trees.mli | 2 +- proofs/proof_type.ml | 2 +- proofs/proof_type.mli | 2 +- proofs/redexpr.ml | 2 +- proofs/redexpr.mli | 2 +- proofs/refiner.ml | 2 +- proofs/refiner.mli | 2 +- proofs/tacexpr.ml | 2 +- proofs/tacmach.ml | 2 +- proofs/tacmach.mli | 2 +- proofs/tactic_debug.ml | 2 +- proofs/tactic_debug.mli | 2 +- 24 files changed, 25 insertions(+), 25 deletions(-) (limited to 'proofs') 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 -- cgit v1.2.3