aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/classops.ml72
-rw-r--r--pretyping/classops.mli4
-rw-r--r--pretyping/coercion.ml8
-rw-r--r--pretyping/constr_matching.ml11
-rw-r--r--pretyping/evarconv.ml17
-rw-r--r--pretyping/geninterp.ml7
-rw-r--r--pretyping/geninterp.mli7
-rw-r--r--pretyping/globEnv.ml6
-rw-r--r--pretyping/globEnv.mli4
-rw-r--r--pretyping/glob_ops.ml11
-rw-r--r--pretyping/glob_ops.mli2
-rw-r--r--pretyping/pattern.ml2
-rw-r--r--pretyping/patternops.ml11
-rw-r--r--pretyping/pretyping.ml64
-rw-r--r--pretyping/pretyping.mli1
15 files changed, 120 insertions, 107 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 54a1aa9aa0..5560e5e5f5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -120,9 +120,6 @@ let class_tab =
let coercion_tab =
Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
-let coercions_in_scope =
- Summary.ref ~name:"coercions_in_scope" GlobRef.Set_env.empty
-
module ClPairOrd =
struct
type t = cl_index * cl_index
@@ -308,9 +305,16 @@ let install_path_printer f = path_printer := f
let print_path x = !path_printer x
-let message_ambig l =
- str"Ambiguous paths:" ++ spc () ++
- prlist_with_sep fnl print_path l
+let path_comparator : (inheritance_path -> inheritance_path -> bool) ref =
+ ref (fun _ _ -> false)
+
+let install_path_comparator f = path_comparator := f
+
+let compare_path p q = !path_comparator p q
+
+let warn_ambiguous_path =
+ CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
+ (fun l -> strbrk"Ambiguous paths: " ++ prlist_with_sep fnl print_path l)
(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
coercion,source,target *)
@@ -329,21 +333,15 @@ let add_coercion_in_graph (ic,source,target) =
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
let try_add_new_path (i,j as ij) p =
- try
- if Bijint.Index.equal i j then begin
- if different_class_params i then begin
- let _ = lookup_path_between_class ij in
- ambig_paths := (ij,p)::!ambig_paths
- end
- end else begin
- let _ = lookup_path_between_class ij in
- ambig_paths := (ij,p)::!ambig_paths
- end;
+ if not (Bijint.Index.equal i j) || different_class_params i then
+ match lookup_path_between_class ij with
+ | q ->
+ if not (compare_path p q) then
+ ambig_paths := (ij,p)::!ambig_paths;
+ false
+ | exception Not_found -> (add_new_path ij p; true)
+ else
false
- with Not_found -> begin
- add_new_path ij p;
- true
- end
in
let try_add_new_path1 ij p =
let _ = try_add_new_path ij p in ()
@@ -364,9 +362,7 @@ let add_coercion_in_graph (ic,source,target) =
end)
old_inheritance_graph
end;
- let is_ambig = match !ambig_paths with [] -> false | _ -> true in
- if is_ambig && not !Flags.quiet then
- Feedback.msg_info (message_ambig !ambig_paths)
+ match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
type coercion = {
coercion_type : coe_typ;
@@ -400,13 +396,6 @@ let class_params = function
let add_class cl =
add_new_class cl { cl_param = class_params cl }
-let get_automatically_import_coercions =
- Goptions.declare_bool_option_and_ref
- ~depr:true (* Remove in 8.8 *)
- ~name:"automatic import of coercions"
- ~key:["Automatic";"Coercions";"Import"]
- ~value:false
-
let cache_coercion (_, c) =
let () = add_class c.coercion_source in
let () = add_class c.coercion_target in
@@ -422,20 +411,9 @@ let cache_coercion (_, c) =
let () = add_new_coercion c.coercion_type xf in
add_coercion_in_graph (xf,is,it)
-let load_coercion _ o =
- if get_automatically_import_coercions () then
- cache_coercion o
-
-let set_coercion_in_scope (_, c) =
- let r = c.coercion_type in
- coercions_in_scope := GlobRef.Set_env.add r !coercions_in_scope
-
let open_coercion i o =
- if Int.equal i 1 then begin
- set_coercion_in_scope o;
- if not (get_automatically_import_coercions ()) then
- cache_coercion o
- end
+ if Int.equal i 1 then
+ cache_coercion o
let subst_coercion (subst, c) =
let coe = subst_coe_typ subst c.coercion_type in
@@ -469,10 +447,7 @@ let classify_coercion obj =
let inCoercion : coercion -> obj =
declare_object {(default_object "COERCION") with
open_function = open_coercion;
- load_function = load_coercion;
- cache_function = (fun objn ->
- set_coercion_in_scope objn;
- cache_coercion objn);
+ cache_function = cache_coercion;
subst_function = subst_coercion;
classify_function = classify_coercion;
discharge_function = discharge_coercion }
@@ -532,6 +507,3 @@ let hide_coercion coe =
let coe_info = coercion_info coe in
Some coe_info.coe_param
else None
-
-let is_coercion_in_scope r =
- GlobRef.Set_env.mem r !coercions_in_scope
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index 7c4842c8ae..bd468e62ad 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -100,6 +100,8 @@ val lookup_pattern_path_between :
(* Crade *)
val install_path_printer :
((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+val install_path_comparator :
+ (inheritance_path -> inheritance_path -> bool) -> unit
(**/**)
(** {6 This is for printing purpose } *)
@@ -113,5 +115,3 @@ 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 *)
val hide_coercion : coe_typ -> int option
-
-val is_coercion_in_scope : GlobRef.t -> bool
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 82411ba2ef..8c9b6550f3 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -368,20 +368,12 @@ let saturate_evd env evd =
Typeclasses.resolve_typeclasses
~filter:Typeclasses.no_goals ~split:true ~fail:false env evd
-let warn_coercion_not_in_scope =
- CWarnings.create ~name:"coercion-not-in-scope" ~category:"deprecated"
- Pp.(fun r -> str "Coercion used but not in scope: " ++
- Nametab.pr_global_env Id.Set.empty r ++ str ". If you want to use "
- ++ str "this coercion, please Import the module that contains it.")
-
(* Apply coercion path from p to hj; raise NoCoercion if not applicable *)
let apply_coercion env sigma p hj typ_cl =
try
let j,t,evd =
List.fold_left
(fun (ja,typ_cl,sigma) i ->
- if not (is_coercion_in_scope i.coe_value) then
- warn_coercion_not_in_scope i.coe_value;
let isid = i.coe_is_identity in
let isproj = i.coe_is_projection in
let sigma, c = new_global sigma i.coe_value in
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index bc083ed9d9..6bfbb9a9c0 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -17,7 +17,6 @@ open Constr
open Context
open Globnames
open Termops
-open Term
open EConstr
open Vars
open Pattern
@@ -280,14 +279,8 @@ let matches_core env sigma allow_bound_rels
| PRel n1, Rel n2 when Int.equal n1 n2 -> subst
| PSort ps, Sort s ->
-
- let open Glob_term in
- begin match ps, ESorts.kind sigma s with
- | GProp, Prop -> subst
- | GSet, Set -> subst
- | GType _, Type _ -> subst
- | _ -> raise PatternMatchingFailure
- end
+ if Sorts.family_equal ps (Sorts.family (ESorts.kind sigma s))
+ then subst else raise PatternMatchingFailure
| PApp (p, [||]), _ -> sorec ctx env subst p t
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 28a97bb91a..0ccc4fd9f9 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -503,14 +503,23 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
| Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem true pbty,ev,term2) with
- | UnifFailure (_,OccurCheck _) ->
- (* Eta-expansion might apply *) default ()
+ | UnifFailure (_,(OccurCheck _ | NotClean _)) ->
+ (* Eta-expansion might apply *)
+ (* OccurCheck: eta-expansion could solve
+ ?X = {| foo := ?X.(foo) |}
+ NotClean: pruning in solve_simple_eqn is incomplete wrt
+ Miller patterns *)
+ default ()
| x -> x)
| _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem false pbty,ev,term1) with
- | UnifFailure (_, OccurCheck _) ->
- (* Eta-expansion might apply *) default ()
+ | UnifFailure (_, (OccurCheck _ | NotClean _)) ->
+ (* OccurCheck: eta-expansion could solve
+ ?X = {| foo := ?X.(foo) |}
+ NotClean: pruning in solve_simple_eqn is incomplete wrt
+ Miller patterns *)
+ default ()
| x -> x)
| _ -> default ()
end
diff --git a/pretyping/geninterp.ml b/pretyping/geninterp.ml
index 1f8b926365..32152ad0e4 100644
--- a/pretyping/geninterp.ml
+++ b/pretyping/geninterp.ml
@@ -82,9 +82,10 @@ let register_val0 wit tag =
(** Interpretation functions *)
-type interp_sign = {
- lfun : Val.t Id.Map.t;
- extra : TacStore.t }
+type interp_sign =
+ { lfun : Val.t Id.Map.t
+ ; poly : bool
+ ; extra : TacStore.t }
type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
diff --git a/pretyping/geninterp.mli b/pretyping/geninterp.mli
index 606a6ebead..49d874289d 100644
--- a/pretyping/geninterp.mli
+++ b/pretyping/geninterp.mli
@@ -62,9 +62,10 @@ val register_val0 : ('raw, 'glb, 'top) genarg_type -> 'top Val.tag option -> uni
module TacStore : Store.S
-type interp_sign = {
- lfun : Val.t Id.Map.t;
- extra : TacStore.t }
+type interp_sign =
+ { lfun : Val.t Id.Map.t
+ ; poly : bool
+ ; extra : TacStore.t }
type ('glb, 'top) interp_fun = interp_sign -> 'glb -> 'top Ftactic.t
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index cd82b1993b..e76eb2a7de 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -183,7 +183,7 @@ let interp_ltac_id env id = ltac_interp_id env.lvar id
module ConstrInterpObj =
struct
type ('r, 'g, 't) obj =
- unbound_ltac_var_map -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
+ unbound_ltac_var_map -> bool -> env -> Evd.evar_map -> types -> 'g -> constr * Evd.evar_map
let name = "constr_interp"
let default _ = None
end
@@ -192,8 +192,8 @@ module ConstrInterp = Genarg.Register(ConstrInterpObj)
let register_constr_interp0 = ConstrInterp.register0
-let interp_glob_genarg env sigma ty arg =
+let interp_glob_genarg env poly sigma ty arg =
let open Genarg in
let GenArg (Glbwit tag, arg) = arg in
let interp = ConstrInterp.obj tag in
- interp env.lvar.ltac_genargs env.renamed_env sigma ty arg
+ interp env.lvar.ltac_genargs poly env.renamed_env sigma ty arg
diff --git a/pretyping/globEnv.mli b/pretyping/globEnv.mli
index 65ae495135..cdd36bbba6 100644
--- a/pretyping/globEnv.mli
+++ b/pretyping/globEnv.mli
@@ -19,7 +19,7 @@ open Evarutil
val register_constr_interp0 :
('r, 'g, 't) Genarg.genarg_type ->
- (unbound_ltac_var_map -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
+ (unbound_ltac_var_map -> bool -> env -> evar_map -> types -> 'g -> constr * evar_map) -> unit
(** {6 Pretyping name management} *)
@@ -85,5 +85,5 @@ val interp_ltac_id : t -> Id.t -> Id.t
(** Interpreting a generic argument, typically a "ltac:(...)", taking
into account the possible renaming *)
-val interp_glob_genarg : t -> evar_map -> constr ->
+val interp_glob_genarg : t -> bool -> evar_map -> constr ->
Genarg.glob_generic_argument -> constr * evar_map
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index affed5389f..74432cc010 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -47,11 +47,18 @@ let map_glob_decl_left_to_right f (na,k,obd,ty) =
let glob_sort_eq g1 g2 = let open Glob_term in match g1, g2 with
-| GProp, GProp -> true
+| GSProp, GSProp
+| GProp, GProp
| GSet, GSet -> true
| GType l1, GType l2 ->
List.equal (Option.equal (fun (x,m) (y,n) -> Libnames.qualid_eq x y && Int.equal m n)) l1 l2
-| _ -> false
+| (GSProp|GProp|GSet|GType _), _ -> false
+
+let glob_sort_family = let open Sorts in function
+| GSProp -> InSProp
+| GProp -> InProp
+| GSet -> InSet
+| GType _ -> InType
let binding_kind_eq bk1 bk2 = match bk1, bk2 with
| Decl_kinds.Explicit, Decl_kinds.Explicit -> true
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index c189a3bcb2..2f0ac76235 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -15,6 +15,8 @@ open Glob_term
val glob_sort_eq : Glob_term.glob_sort -> Glob_term.glob_sort -> bool
+val glob_sort_family : 'a glob_sort_gen -> Sorts.family
+
val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
val alias_of_pat : 'a cases_pattern_g -> Name.t
diff --git a/pretyping/pattern.ml b/pretyping/pattern.ml
index 2ca7f21e8d..d1c0a4ea2a 100644
--- a/pretyping/pattern.ml
+++ b/pretyping/pattern.ml
@@ -32,7 +32,7 @@ type constr_pattern =
| PLambda of Name.t * constr_pattern * constr_pattern
| PProd of Name.t * constr_pattern * constr_pattern
| PLetIn of Name.t * constr_pattern * constr_pattern option * constr_pattern
- | PSort of Glob_term.glob_sort
+ | PSort of Sorts.family
| PMeta of patvar option
| PIf of constr_pattern * constr_pattern * constr_pattern
| PCase of case_info_pattern * constr_pattern * constr_pattern *
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 13034d078a..4e3c77cb1a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -13,7 +13,6 @@ open Util
open Names
open Globnames
open Nameops
-open Term
open Constr
open Context
open Glob_term
@@ -47,7 +46,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
| PLetIn (v1, b1, t1, c1), PLetIn (v2, b2, t2, c2) ->
Name.equal v1 v2 && constr_pattern_eq b1 b2 &&
Option.equal constr_pattern_eq t1 t2 && constr_pattern_eq c1 c2
-| PSort s1, PSort s2 -> Glob_ops.glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Sorts.family_equal s1 s2
| PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
| PIf (t1, l1, r1), PIf (t2, l2, r2) ->
constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
@@ -154,10 +153,7 @@ let pattern_of_constr env sigma t =
| Rel n -> PRel n
| Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
| Var id -> PVar id
- | Sort SProp -> PSort GSProp
- | Sort Prop -> PSort GProp
- | Sort Set -> PSort GSet
- | Sort (Type _) -> PSort (GType [])
+ | Sort s -> PSort (Sorts.family s)
| Cast (c,_,_) -> pattern_of_constr env c
| LetIn (na,c,t,b) -> PLetIn (na.binder_name,
pattern_of_constr env c,Some (pattern_of_constr env t),
@@ -416,8 +412,7 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
PLetIn (na, pat_of_raw metas vars c1,
Option.map (pat_of_raw metas vars) t,
pat_of_raw metas (na::vars) c2)
- | GSort s ->
- PSort s
+ | GSort gs -> PSort (Glob_ops.glob_sort_family gs)
| GHole _ ->
PMeta None
| GCast (c,_) ->
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8e9a2e114b..bec939b911 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -198,6 +198,7 @@ type inference_flags = {
fail_evar : bool;
expand_evars : bool;
program_mode : bool;
+ polymorphic : bool;
}
(* Compute the set of still-undefined initial evars up to restriction
@@ -474,10 +475,10 @@ let mark_obligation_evar sigma k evc =
(* in environment [env], with existential variables [sigma] and *)
(* the type constraint tycon *)
-let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
+let rec pretype ~program_mode ~poly k0 resolve_tc (tycon : type_constraint) (env : GlobEnv.t) (sigma : evar_map) t =
let inh_conv_coerce_to_tycon ?loc = inh_conv_coerce_to_tycon ?loc ~program_mode resolve_tc in
- let pretype_type = pretype_type ~program_mode k0 resolve_tc in
- let pretype = pretype ~program_mode k0 resolve_tc in
+ let pretype_type = pretype_type ~program_mode ~poly k0 resolve_tc in
+ let pretype = pretype ~program_mode ~poly k0 resolve_tc in
let open Context.Rel.Declaration in
let loc = t.CAst.loc in
match DAst.get t with
@@ -497,7 +498,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
try Evd.evar_key id sigma
with Not_found -> error_evar_not_found ?loc !!env sigma id in
let hyps = evar_filtered_context (Evd.find sigma evk) in
- let sigma, args = pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk inst in
+ let sigma, args = pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk inst in
let c = mkEvar (evk, args) in
let j = Retyping.get_judgment_of !!env sigma c in
inh_conv_coerce_to_tycon ?loc env sigma j tycon
@@ -530,7 +531,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
match tycon with
| Some ty -> sigma, ty
| None -> new_type_evar env sigma loc in
- let c, sigma = GlobEnv.interp_glob_genarg env sigma ty arg in
+ let c, sigma = GlobEnv.interp_glob_genarg env poly sigma ty arg in
sigma, { uj_val = c; uj_type = ty }
| GRec (fixkind,names,bl,lar,vdef) ->
@@ -983,7 +984,7 @@ let rec pretype ~program_mode k0 resolve_tc (tycon : type_constraint) (env : Glo
in
inh_conv_coerce_to_tycon ?loc env sigma resj tycon
-and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
+and pretype_instance ~program_mode ~poly k0 resolve_tc env sigma loc hyps evk update =
let f decl (subst,update,sigma) =
let id = NamedDecl.get_id decl in
let b = Option.map (replace_vars subst) (NamedDecl.get_value decl) in
@@ -1015,7 +1016,7 @@ and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
let sigma, c, update =
try
let c = List.assoc id update in
- let sigma, c = pretype ~program_mode k0 resolve_tc (mk_tycon t) env sigma c in
+ let sigma, c = pretype ~program_mode ~poly k0 resolve_tc (mk_tycon t) env sigma c in
check_body sigma id (Some c.uj_val);
sigma, c.uj_val, List.remove_assoc id update
with Not_found ->
@@ -1040,7 +1041,7 @@ and pretype_instance ~program_mode k0 resolve_tc env sigma loc hyps evk update =
sigma, Array.map_of_list snd subst
(* [pretype_type valcon env sigma c] coerces [c] into a type *)
-and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
+and pretype_type ~program_mode ~poly k0 resolve_tc valcon (env : GlobEnv.t) sigma c = match DAst.get c with
| GHole (knd, naming, None) ->
let loc = loc_of_glob_constr c in
(match valcon with
@@ -1067,7 +1068,7 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
let sigma = if program_mode then mark_obligation_evar sigma knd utj_val else sigma in
sigma, { utj_val; utj_type = s})
| _ ->
- let sigma, j = pretype ~program_mode k0 resolve_tc empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode ~poly k0 resolve_tc empty_tycon env sigma c in
let loc = loc_of_glob_constr c in
let sigma, tj = Coercion.inh_coerce_to_sort ?loc !!env sigma j in
match valcon with
@@ -1082,6 +1083,7 @@ and pretype_type ~program_mode k0 resolve_tc valcon (env : GlobEnv.t) sigma c =
let ise_pretype_gen flags env sigma lvar kind c =
let program_mode = flags.program_mode in
+ let poly = flags.polymorphic in
let hypnaming =
if program_mode then ProgramNaming else KeepUserNameAndRenameExistingButSectionNames
in
@@ -1089,13 +1091,13 @@ let ise_pretype_gen flags env sigma lvar kind c =
let k0 = Context.Rel.length (rel_context !!env) in
let sigma', c', c'_ty = match kind with
| WithoutTypeConstraint ->
- let sigma, j = pretype ~program_mode k0 flags.use_typeclasses empty_tycon env sigma c in
+ let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses empty_tycon env sigma c in
sigma, j.uj_val, j.uj_type
| OfType exptyp ->
- let sigma, j = pretype ~program_mode k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
+ let sigma, j = pretype ~program_mode ~poly k0 flags.use_typeclasses (mk_tycon exptyp) env sigma c in
sigma, j.uj_val, j.uj_type
| IsType ->
- let sigma, tj = pretype_type ~program_mode k0 flags.use_typeclasses empty_valcon env sigma c in
+ let sigma, tj = pretype_type ~program_mode ~poly k0 flags.use_typeclasses empty_valcon env sigma c in
sigma, tj.utj_val, mkSort tj.utj_type
in
process_inference_flags flags !!env sigma (sigma',c',c'_ty)
@@ -1106,6 +1108,7 @@ let default_inference_flags fail = {
fail_evar = fail;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
let no_classes_no_fail_inference_flags = {
@@ -1114,6 +1117,7 @@ let no_classes_no_fail_inference_flags = {
fail_evar = false;
expand_evars = true;
program_mode = false;
+ polymorphic = false;
}
let all_and_fail_flags = default_inference_flags true
@@ -1141,3 +1145,39 @@ let understand_tcc ?flags env sigma ?expected_type c =
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 open Classops in
+ let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in
+ let mkGVar id = DAst.make @@ Glob_term.GVar(id) in
+ let mkGApp(rt,rtl) = DAst.make @@ Glob_term.GApp(rt,rtl) in
+ let mkGLambda(n,t,b) = DAst.make @@ Glob_term.GLambda(n,Decl_kinds.Explicit,t,b) in
+ let mkGHole () = DAst.make @@ Glob_term.GHole(Evar_kinds.BinderType Anonymous,Namegen.IntroAnonymous,None) in
+ let path_to_gterm p =
+ match p with
+ | ic :: p' ->
+ let names =
+ List.map (fun n -> Id.of_string ("x" ^ string_of_int n))
+ (List.interval 0 ic.coe_param)
+ in
+ List.fold_right
+ (fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
+ List.fold_left
+ (fun t ic ->
+ mkGApp (mkGRef ic.coe_value,
+ List.make ic.coe_param (mkGHole ()) @ [t]))
+ (mkGApp (mkGRef ic.coe_value, List.map (fun i -> mkGVar i) names))
+ p'
+ | [] -> 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
+ if Evd.has_undefined sigma then
+ false
+ else
+ let _ = Evarconv.unify_delay e sigma tp tq in true
+ with Evarconv.UnableToUnify _ | PretypeError _ -> false
+
+let _ = Classops.install_path_comparator path_convertible
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 3c875e69d2..1037cf6cc5 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -38,6 +38,7 @@ type inference_flags = {
fail_evar : bool;
expand_evars : bool;
program_mode : bool;
+ polymorphic : bool;
}
val default_inference_flags : bool -> inference_flags
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-05 04:55:24 +0000