Merge PR #8103: Coercions cleanup: use GlobRef.t instead of constr

6 files changed, 45 insertions, 63 deletions

diff --git a/plugins/firstorder/ground.ml b/plugins/firstorder/ground.ml
index 4e3ba57308..516b04ea21 100644
--- a/plugins/firstorder/ground.ml
+++ b/plugins/firstorder/ground.ml
@@ -13,23 +13,21 @@ 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 acc coe =
+    match coe.Classops.coe_value with
+    | ConstRef c -> Names.Cpred.add c acc
+    | _ -> acc
   in
-    List.iter f (Classops.coercions ());
+    let pred = List.fold_left f Names.Cpred.empty (Classops.coercions ()) in
     red_flags:=
     CClosure.RedFlags.red_add_transparent
       CClosure.betaiotazeta
-      (Names.Id.Pred.full,Names.Cpred.complement !predref)
+      (Names.Id.Pred.full,Names.Cpred.complement pred)
 
 let ground_tac solver startseq =
   Proofview.Goal.enter begin fun gl ->
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
 
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 7ac08e755e..542fb5456c 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -42,18 +42,15 @@ type coe_typ = GlobRef.t
 module CoeTypMap = Refmap_env
 
 type coe_info_typ = {
-  coe_value : constr;
-  coe_type : types;
+  coe_value : GlobRef.t;
   coe_local : bool;
-  coe_context : Univ.ContextSet.t;
   coe_is_identity : bool;
   coe_is_projection : Projection.Repr.t option;
-  coe_param : int }
+  coe_param : int;
+}
 
 let coe_info_typ_equal c1 c2 =
-  let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in
-  eq_constr c1.coe_value c2.coe_value &&
-    eq_constr c1.coe_type c2.coe_type &&
+  GlobRef.equal c1.coe_value c2.coe_value &&
     c1.coe_local == c2.coe_local &&
     c1.coe_is_identity == c2.coe_is_identity &&
     c1.coe_is_projection == c2.coe_is_projection &&
@@ -77,9 +74,7 @@ module IntMap = Map.Make(Int)
 
 let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
 
-type coe_index = coe_info_typ
-
-type inheritance_path = coe_index list
+type inheritance_path = coe_info_typ list
 
 (* table des classes, des coercions et graphe d'heritage *)
 
@@ -300,31 +295,25 @@ let lookup_path_to_fun_from env sigma s =
 let lookup_path_to_sort_from env sigma s =
   apply_on_class_of env sigma s lookup_path_to_sort_from_class
 
+let mkNamed = function
+  | GlobRef.ConstRef c -> EConstr.mkConst c
+  | VarRef v -> EConstr.mkVar v
+  | ConstructRef c -> EConstr.mkConstruct c
+  | IndRef i -> EConstr.mkInd i
+
 let get_coercion_constructor env coe =
-  let c, _ =
-    Reductionops.whd_all_stack env Evd.empty (EConstr.of_constr coe.coe_value)
-  in
-  match EConstr.kind Evd.empty (** FIXME *) c with
-  | Construct (cstr,u) ->
-      (cstr, Inductiveops.constructor_nrealargs cstr -1)
-  | _ ->
-      raise Not_found
+  let evd = Evd.from_env env in
+  let red x = fst (Reductionops.whd_all_stack env evd x) in
+  match EConstr.kind evd (red (mkNamed coe.coe_value)) with
+  | Constr.Construct (c, _) ->
+      c, Inductiveops.constructor_nrealargs c -1
+  | _ -> raise Not_found
 
 let lookup_pattern_path_between env (s,t) =
   let i = inductive_class_of s in
   let j = inductive_class_of t in
   List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph)
 
-(* coercion_value : coe_index -> unsafe_judgment * bool *)
-
-let coercion_value { coe_value = c; coe_type = t; coe_context = ctx; 
-		     coe_is_identity = b; coe_is_projection = b' } =
-  let subst, ctx = UnivGen.fresh_universe_context_set_instance ctx in
-  let c' = Vars.subst_univs_level_constr subst c 
-  and t' = Vars.subst_univs_level_constr subst t in
-    (make_judge (EConstr.of_constr c') (EConstr.of_constr t'), b, b'), ctx
-
-(* pretty-print functions are now in Pretty *)
 (* rajouter une coercion dans le graphe *)
 
 let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t) ref =
@@ -442,17 +431,13 @@ let cache_coercion env sigma (_, c) =
   let () = add_class c.coercion_target in
   let is, _ = class_info c.coercion_source in
   let it, _ = class_info c.coercion_target in
-  let value, ctx = UnivGen.fresh_global_instance env c.coercion_type in
-  let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in
-  let typ = EConstr.Unsafe.to_constr typ in
   let xf =
-    { coe_value = value;
-      coe_type = typ;
-      coe_context = ctx;
+    { coe_value = c.coercion_type;
       coe_local = c.coercion_local;
       coe_is_identity = c.coercion_is_id;
       coe_is_projection = c.coercion_is_proj;
-      coe_param = c.coercion_params } in
+      coe_param = c.coercion_params;
+    } in
   let () = add_new_coercion c.coercion_type xf in
   add_coercion_in_graph env sigma (xf,is,it)
 
@@ -531,8 +516,6 @@ let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps
   Lib.add_anonymous_leaf (inCoercion c)
 
 (* For printing purpose *)
-let get_coercion_value v = v.coe_value
-
 let pr_cl_index = Bijint.Index.print
 
 let classes () = Bijint.dom !class_tab
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 8df085e15c..af00c0a8dc 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -39,16 +39,19 @@ type cl_info_typ = {
 type coe_typ = GlobRef.t
 
 (** This is the type of infos for declared coercions *)
-type coe_info_typ
+type coe_info_typ = {
+  coe_value : GlobRef.t;
+  coe_local : bool;
+  coe_is_identity : bool;
+  coe_is_projection : Projection.Repr.t option;
+  coe_param : int;
+}
 
 (** [cl_index] is the type of class keys *)
 type cl_index
 
-(** [coe_index] is the type of coercion keys *)
-type coe_index
-
 (** This is the type of paths from a class to another *)
-type inheritance_path = coe_index list
+type inheritance_path = coe_info_typ list
 
 (** {6 Access to classes infos } *)
 
@@ -79,8 +82,6 @@ val declare_coercion :
 (** {6 Access to coercions infos } *)
 val coercion_exists : coe_typ -> bool
 
-val coercion_value : coe_index -> (unsafe_judgment * bool * Projection.Repr.t option) Univ.in_universe_context_set
-
 (** {6 Lookup functions for coercion paths } *)
 
 (** @raise Not_found in the following functions when no path exists *)
@@ -105,10 +106,9 @@ val install_path_printer :
 val string_of_class : cl_typ -> string
 val pr_class : cl_typ -> Pp.t
 val pr_cl_index : cl_index -> Pp.t
-val get_coercion_value : coe_index -> Constr.t
 val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
 val classes : unit -> cl_typ list
-val coercions : unit -> coe_index list
+val coercions : unit -> coe_info_typ list
 
 (** [hide_coercion] returns the number of params to skip if the coercion must
    be hidden, [None] otherwise; it raises [Not_found] if not a coercion *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index c6c2f57dd4..5e3821edf1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -369,8 +369,11 @@ let apply_coercion env sigma p hj typ_cl =
     let j,t,evd = 
       List.fold_left
         (fun (ja,typ_cl,sigma) i ->
-	  let ((fv,isid,isproj),ctx) = coercion_value i in
-	  let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+           let isid = i.coe_is_identity in
+           let isproj = i.coe_is_projection in
+           let sigma, c = new_global sigma i.coe_value in
+           let typ = Retyping.get_type_of env sigma c in
+           let fv = make_judge c typ in
 	  let argl = (class_args_of env sigma typ_cl)@[ja.uj_val] in
 	  let sigma, jres = 
 	    apply_coercion_args env sigma true isproj argl fv 
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index 8b835310de..1810cc6588 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -902,7 +902,7 @@ let inspect env sigma depth =
 
 open Classops
 
-let print_coercion_value env sigma v = pr_lconstr_env env sigma (get_coercion_value v)
+let print_coercion_value env sigma v = Printer.pr_global v.coe_value
 
 let print_class i =
   let cl,_ = class_info_from_index i in