diff options
| author | Enrico Tassi | 2018-07-27 08:55:30 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2018-07-27 08:55:30 +0200 |
| commit | e7c1b08bbb300d31e82ca6c457fd4e3050239b9d (patch) | |
| tree | 6813ef46499b6de0d532d97946374e274e587b58 /plugins/ssr | |
| parent | 9f9a7736c24270a3f3d8177c65e80a1ee04c4615 (diff) | |
| parent | baf8b6e100c49635c56308f17275b963d4f5253c (diff) | |
Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constr
Diffstat (limited to 'plugins/ssr')
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4 index 7ce2dd64af..8ce0316f53 100644 --- a/plugins/ssr/ssrvernac.ml4 +++ b/plugins/ssr/ssrvernac.ml4 @@ -24,7 +24,6 @@ open Ltac_plugin open Notation_ops open Notation_term open Glob_term -open Globnames open Stdarg open Genarg open Decl_kinds @@ -359,13 +358,12 @@ let coerce_search_pattern_to_sort hpat = true, cp with _ -> false, [] in let coerce hp coe_index = - let coe = Classops.get_coercion_value coe_index in + let coe_ref = coe_index.Classops.coe_value in try - let coe_ref = global_of_constr coe in let n_imps = Option.get (Classops.hide_coercion coe_ref) in mkPApp (Pattern.PRef coe_ref) n_imps [|hp|] - with _ -> - errorstrm (str "need explicit coercion " ++ pr_constr_env env sigma coe ++ spc () + with Not_found | Option.IsNone -> + errorstrm (str "need explicit coercion " ++ pr_global coe_ref ++ spc () ++ str "to interpret head search pattern as type") in filter_head, List.fold_left coerce hpat' coe_path |