diff options
| author | Maxime Dénès | 2018-07-20 18:01:18 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-07-26 14:42:45 +0200 |
| commit | f54192a50eaf14852e1462f24e4168aa8a8545fe (patch) | |
| tree | 64696d9c111f420e9bff7d7f742602a6b38f8b0a /plugins | |
| parent | 85d5f45d7a5374646a31f8829965bbfed0a95070 (diff) | |
Coercions cleanup: use GlobRef.t instead of constr
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/firstorder/ground.ml | 11 | ||||
| -rw-r--r-- | plugins/ssr/ssrvernac.ml4 | 8 |
2 files changed, 8 insertions, 11 deletions
diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml index 4e3ba57308..3901a951f0 100644 --- a/plugins/firstorder/ground.ml +++ b/plugins/firstorder/ground.ml @@ -13,17 +13,16 @@ open Formula open Sequent open Rules open Instances -open Constr open Tacmach.New open Tacticals.New +open Globnames let update_flags ()= let predref=ref Names.Cpred.empty in - let f coe= - try - let kn= fst (destConst (Classops.get_coercion_value coe)) in - predref:=Names.Cpred.add kn !predref - with DestKO -> () + let f coe = + match coe.Classops.coe_value with + | ConstRef c -> predref := Names.Cpred.add c !predref + | _ -> () in List.iter f (Classops.coercions ()); red_flags:= 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 |