diff options
| author | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2019-12-23 22:57:20 +0100 |
| commit | 028d64fb5c461e32752b0f8a92d4e2eca2a26d0d (patch) | |
| tree | 8380a901d2c066536f38552f67ffa76f0e3364b3 /vernac/comAssumption.ml | |
| parent | 3b9763487f96d308f6339c7eb4fc834b069f6e40 (diff) | |
| parent | cc3ded87f0f440eac2746d59b7aeba60ca9f691f (diff) | |
Merge PR #11293: Rename files with Class in their name to make their role clearer.
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index 8a403e5a03..625ffb5a06 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -32,7 +32,7 @@ let declare_variable is_coe ~kind typ imps impl {CAst.v=name} = let env = Global.env () in let sigma = Evd.from_env env in let () = Classes.declare_instance env sigma None true r in - let () = if is_coe then Class.try_add_new_coercion r ~local:true ~poly:false in + let () = if is_coe then ComCoercion.try_add_new_coercion r ~local:true ~poly:false in () let instance_of_univ_entry = function @@ -65,7 +65,7 @@ let declare_axiom is_coe ~poly ~local ~kind typ (univs, pl) imps nl {CAst.v=name | Declare.ImportNeedQualified -> true | Declare.ImportDefaultBehavior -> false in - let () = if is_coe then Class.try_add_new_coercion gr ~local ~poly in + let () = if is_coe then ComCoercion.try_add_new_coercion gr ~local ~poly in let inst = instance_of_univ_entry univs in (gr,inst) |
