aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/xml/doubleTypeInference.ml
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/xml/doubleTypeInference.ml')
-rw-r--r--contrib/xml/doubleTypeInference.ml26
1 files changed, 13 insertions, 13 deletions
diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml
index 3c5362509..f0e3f5e35 100644
--- a/contrib/xml/doubleTypeInference.ml
+++ b/contrib/xml/doubleTypeInference.ml
@@ -1,16 +1,16 @@
-(***********************************************************************)
-(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
-(* \VV/ *************************************************************)
-(* // * The HELM Project / The EU MoWGLI Project *)
-(* * University of Bologna *)
-(***********************************************************************)
-(* This file is distributed under the terms of the *)
-(* GNU Lesser General Public License Version 2.1 *)
-(* *)
-(* Copyright (C) 2000-2004, HELM Team. *)
-(* http://helm.cs.unibo.it *)
-(***********************************************************************)
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * The HELM Project / The EU MoWGLI Project *)
+(* * University of Bologna *)
+(************************************************************************)
+(* This file is distributed under the terms of the *)
+(* GNU Lesser General Public License Version 2.1 *)
+(* *)
+(* Copyright (C) 2000-2004, HELM Team. *)
+(* http://helm.cs.unibo.it *)
+(************************************************************************)
(*CSC: tutto da rifare!!! Basarsi su Retyping che e' meno costoso! *)
type types = {synthesized : Term.types ; expected : Term.types option};;