diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 12:48:32 +0100 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2014-12-09 14:27:21 +0100 |
| commit | af84e080ff674a3d5cf2cf88874ddb6ebaf38ecf (patch) | |
| tree | b8325cd8ce34dd2dcfba2792a0123cf8c46ab703 /pretyping/coercion.ml | |
| parent | 9c24cecec3a7381cd924c56ca50c77a49750e2e5 (diff) | |
Switch the few remaining iso-latin-1 files to utf8
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 504d73cb8..ae9210e49 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -9,7 +9,7 @@ (* Created by Hugo Herbelin for Coq V7 by isolating the coercion mechanism out of the type inference algorithm in file trad.ml from Coq V6.3, Nov 1999; The coercion mechanism was implemented in - trad.ml by Amokrane Saïbi, May 1996 *) + trad.ml by Amokrane Saïbi, May 1996 *) (* Addition of products and sorts in canonical structures by Pierre Corbineau, Feb 2008 *) (* Turned into an abstract compilation unit by Matthieu Sozeau, March 2006 *) @@ -345,7 +345,7 @@ let saturate_evd env evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~split:false ~fail:false env evd -(* appliquer le chemin de coercions p à hj *) +(* appliquer le chemin de coercions p à hj *) let apply_coercion env sigma p hj typ_cl = try let j,t,evd = |