aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMaxime Dénès2019-04-05 09:57:49 +0200
committerMaxime Dénès2019-04-10 15:41:44 +0200
commit69c31d24fc8d058070cc7cadc1df28bfac7f6497 (patch)
tree8c50decd7beac16f2cf464641544d0373b455e67
parentac5d50d405ad878b6899d483e64576de63d2d095 (diff)
Remove call to global env in pretyping.ml
-rw-r--r--pretyping/classops.ml10
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/pretyping.ml9
3 files changed, 10 insertions, 11 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 20215029af..0203819051 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -304,8 +304,8 @@ let install_path_printer f = path_printer := f
let print_path x = !path_printer x
-let path_comparator : (inheritance_path -> inheritance_path -> bool) ref =
- ref (fun _ _ -> false)
+let path_comparator : (Environ.env -> Evd.evar_map -> inheritance_path -> inheritance_path -> bool) ref =
+ ref (fun _ _ _ _ -> false)
let install_path_comparator f = path_comparator := f
@@ -327,7 +327,7 @@ let different_class_params env i =
| CL_CONST c -> Environ.is_polymorphic env (ConstRef c)
| _ -> false
-let add_coercion_in_graph env (ic,source,target) =
+let add_coercion_in_graph env sigma (ic,source,target) =
let old_inheritance_graph = !inheritance_graph in
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
@@ -335,7 +335,7 @@ let add_coercion_in_graph env (ic,source,target) =
if not (Bijint.Index.equal i j) || different_class_params env i then
match lookup_path_between_class ij with
| q ->
- if not (compare_path p q) then
+ if not (compare_path env sigma p q) then
ambig_paths := (ij,p)::!ambig_paths;
false
| exception Not_found -> (add_new_path ij p; true)
@@ -419,7 +419,7 @@ let declare_coercion env sigma c =
coe_param = c.coercion_params;
} in
let () = add_new_coercion c.coercion_type xf in
- add_coercion_in_graph env (xf,is,it)
+ add_coercion_in_graph env sigma (xf,is,it)
(* For printing purpose *)
let pr_cl_index = Bijint.Index.print
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 46c6d4c697..c04182930e 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -111,7 +111,7 @@ val lookup_pattern_path_between :
val install_path_printer :
((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
val install_path_comparator :
- (inheritance_path -> inheritance_path -> bool) -> unit
+ (env -> evar_map -> inheritance_path -> inheritance_path -> bool) -> unit
(**/**)
(** {6 This is for printing purpose } *)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index a6e3cfe085..e29672b6bc 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1146,7 +1146,7 @@ let understand_ltac flags env sigma lvar kind c =
let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
(sigma, c)
-let path_convertible p q =
+let path_convertible env sigma p q =
let open Classops in
let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in
let mkGVar id = DAst.make @@ Glob_term.GVar(id) in
@@ -1171,13 +1171,12 @@ let path_convertible p q =
| [] -> anomaly (str "A coercion path shouldn't be empty.")
in
try
- let e = Global.env () in
- let sigma,tp = understand_tcc e (Evd.from_env e) (path_to_gterm p) in
- let sigma,tq = understand_tcc e sigma (path_to_gterm q) in
+ let sigma,tp = understand_tcc env sigma (path_to_gterm p) in
+ let sigma,tq = understand_tcc env sigma (path_to_gterm q) in
if Evd.has_undefined sigma then
false
else
- let _ = Evarconv.unify_delay e sigma tp tq in true
+ let _ = Evarconv.unify_delay env sigma tp tq in true
with Evarconv.UnableToUnify _ | PretypeError _ -> false
let _ = Classops.install_path_comparator path_convertible