1 files changed, 66 insertions, 60 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index a0804b72..52e02c87 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -31,29 +31,26 @@ type cl_typ =
   | CL_SECVAR of variable
   | CL_CONST of Constant.t
   | CL_IND of inductive
-  | CL_PROJ of Constant.t
+  | CL_PROJ of Projection.Repr.t
 
 type cl_info_typ = {
   cl_param : int
 }
 
-type coe_typ = global_reference
+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 : bool;
-  coe_param : int }
+  coe_is_projection : Projection.Repr.t option;
+  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 &&
@@ -62,7 +59,7 @@ let coe_info_typ_equal c1 c2 =
 let cl_typ_ord t1 t2 = match t1, t2 with
   | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
   | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
-  | CL_PROJ c1, CL_PROJ c2 -> Constant.CanOrd.compare c1 c2
+  | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
   | CL_IND i1, CL_IND i2 -> ind_ord i1 i2
   | _ -> Pervasives.compare t1 t2 (** OK *)
 
@@ -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 *)
 
@@ -123,6 +118,9 @@ let class_tab =
 let coercion_tab =
   ref (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
 
+let coercions_in_scope =
+  ref Refset_env.empty
+
 module ClPairOrd =
 struct
   type t = cl_index * cl_index
@@ -136,12 +134,13 @@ module ClPairMap = Map.Make(ClPairOrd)
 let inheritance_graph =
   ref (ClPairMap.empty : inheritance_path ClPairMap.t)
 
-let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph)
+let freeze _ = (!class_tab, !coercion_tab, !inheritance_graph, !coercions_in_scope)
 
-let unfreeze (fcl,fco,fig) =
+let unfreeze (fcl,fco,fig,in_scope) =
   class_tab:=fcl;
   coercion_tab:=fco;
-  inheritance_graph:=fig
+  inheritance_graph:=fig;
+  coercions_in_scope:=in_scope
 
 (* ajout de nouveaux "objets" *)
 
@@ -199,7 +198,7 @@ let find_class_type sigma t =
     | Var id -> CL_SECVAR id, EInstance.empty, args
     | Const (sp,u) -> CL_CONST sp, u, args
     | Proj (p, c) when not (Projection.unfolded p) ->
-      CL_PROJ (Projection.constant p), EInstance.empty, (c :: args)
+      CL_PROJ (Projection.repr p), EInstance.empty, (c :: args)
     | Ind (ind_sp,u) -> CL_IND ind_sp, u, args
     | Prod (_,_,_) -> CL_FUN, EInstance.empty, []
     | Sort _ -> CL_SORT, EInstance.empty, []
@@ -211,7 +210,7 @@ let subst_cl_typ subst ct = match ct with
   | CL_FUN
   | CL_SECVAR _ -> ct
   | CL_PROJ c ->
-    let c',t = subst_con_kn subst c in
+    let c' = subst_proj_repr subst c in
       if c' == c then ct else CL_PROJ c'
   | CL_CONST c ->
       let c',t = subst_con_kn subst c in
@@ -248,8 +247,11 @@ let class_args_of env sigma c = pi3 (find_class_type sigma c)
 let string_of_class = function
   | CL_FUN -> "Funclass"
   | CL_SORT -> "Sortclass"
-  | CL_CONST sp | CL_PROJ sp ->
-      string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+  | CL_CONST sp ->
+    string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
+  | CL_PROJ sp ->
+    let sp = Projection.Repr.constant sp in
+    string_of_qualid (shortest_qualid_of_global Id.Set.empty (ConstRef sp))
   | CL_IND sp ->
       string_of_qualid (shortest_qualid_of_global Id.Set.empty (IndRef sp))
   | CL_SECVAR sp ->
@@ -297,31 +299,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 = Universes.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 =
@@ -395,7 +391,7 @@ type coercion = {
   coercion_type   : coe_typ;
   coercion_local  : bool;
   coercion_is_id  : bool;
-  coercion_is_proj  : bool;
+  coercion_is_proj  : Projection.Repr.t option;
   coercion_source : cl_typ;
   coercion_target : cl_typ;
   coercion_params : int;
@@ -408,9 +404,8 @@ let reference_arity_length ref =
   List.length (fst (Reductionops.splay_arity (Global.env()) Evd.empty (EConstr.of_constr t))) (** FIXME *)
 
 let projection_arity_length p =
-  let len = reference_arity_length (ConstRef p) in
-  let pb = Environ.lookup_projection (Projection.make p false) (Global.env ()) in 
-    len - pb.Declarations.proj_npars
+  let len = reference_arity_length (ConstRef (Projection.Repr.constant p)) in
+  len - Projection.Repr.npars p
 
 let class_params = function
   | CL_FUN | CL_SORT -> 0
@@ -440,17 +435,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 = Universes.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)
 
@@ -458,21 +449,32 @@ let load_coercion _ o =
   if !automatically_import_coercions then
     cache_coercion (Global.env ()) Evd.empty o
 
+let set_coercion_in_scope (_, c) =
+  let r = c.coercion_type in
+  coercions_in_scope := Refset_env.add r !coercions_in_scope
+
 let open_coercion i o =
-  if Int.equal i 1 && not !automatically_import_coercions then
-    cache_coercion (Global.env ()) Evd.empty o
+  if Int.equal i 1 then begin
+    set_coercion_in_scope o;
+    if not !automatically_import_coercions then
+      cache_coercion (Global.env ()) Evd.empty o
+  end
 
 let subst_coercion (subst, c) =
   let coe = subst_coe_typ subst c.coercion_type in
   let cls = subst_cl_typ subst c.coercion_source in
   let clt = subst_cl_typ subst c.coercion_target in
-  if c.coercion_type == coe && c.coercion_source == cls && c.coercion_target == clt then c
-  else { c with coercion_type = coe; coercion_source = cls; coercion_target = clt }
+  let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
+  if c.coercion_type == coe && c.coercion_source == cls &&
+     c.coercion_target == clt && c.coercion_is_proj == clp
+  then c
+  else { c with coercion_type = coe; coercion_source = cls;
+                coercion_target = clt; coercion_is_proj = clp; }
 
 let discharge_cl = function
   | CL_CONST kn -> CL_CONST (Lib.discharge_con kn)
   | CL_IND ind -> CL_IND (Lib.discharge_inductive ind)
-  | CL_PROJ p -> CL_PROJ (Lib.discharge_con p)
+  | CL_PROJ p -> CL_PROJ (Lib.discharge_proj_repr p)
   | cl -> cl
 
 let discharge_coercion (_, c) =
@@ -489,6 +491,7 @@ let discharge_coercion (_, c) =
       coercion_source = discharge_cl c.coercion_source;
       coercion_target = discharge_cl c.coercion_target;
       coercion_params = n + c.coercion_params;
+      coercion_is_proj = Option.map Lib.discharge_proj_repr c.coercion_is_proj;
     } in
     Some nc
 
@@ -500,7 +503,9 @@ let inCoercion : coercion -> obj =
     open_function = open_coercion;
     load_function = load_coercion;
     cache_function = (fun objn ->
-        let env = Global.env () in cache_coercion env Evd.empty objn
+        let env = Global.env () in
+        set_coercion_in_scope objn;
+        cache_coercion env Evd.empty objn
       );
     subst_function = subst_coercion;
     classify_function = classify_coercion;
@@ -509,8 +514,8 @@ let inCoercion : coercion -> obj =
 let declare_coercion coef ?(local = false) ~isid ~src:cls ~target:clt ~params:ps =
   let isproj = 
     match coef with
-    | ConstRef c -> Environ.is_projection c (Global.env ())
-    | _ -> false
+    | ConstRef c -> Recordops.find_primitive_projection c
+    | _ -> None
   in
   let c = {
     coercion_type = coef;
@@ -524,8 +529,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
@@ -563,3 +566,6 @@ let hide_coercion coe =
     let coe_info = coercion_info coe in
     Some coe_info.coe_param
   else None
+
+let is_coercion_in_scope r =
+  Refset_env.mem r !coercions_in_scope