diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index fb11eb558..b0c34e1b4 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -1,10 +1,10 @@ -(***********************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) -(* \VV/ *************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(***********************************************************************) +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) (* $Id$ *) @@ -32,7 +32,7 @@ open Pattern open Dyn -(***********************************************************************) +(************************************************************************) (* This concerns Cases *) open Declarations open Inductive @@ -108,7 +108,7 @@ let transform_rec loc env sigma (pj,c,lf) indt = else mkCase (ci, p, c, lf) -(***********************************************************************) +(************************************************************************) (* To embed constr in rawconstr *) let ((constr_in : constr -> Dyn.t), |