aboutsummaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/btermdn.ml2
-rw-r--r--tactics/btermdn.mli1
-rw-r--r--tactics/class_tactics.ml13
-rw-r--r--tactics/dn.ml20
-rw-r--r--tactics/dn.mli2
-rw-r--r--tactics/equality.ml8
-rw-r--r--tactics/hints.ml134
-rw-r--r--tactics/hints.mli11
-rw-r--r--tactics/inv.ml14
9 files changed, 90 insertions, 115 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml
index bacb5a7b8f..f721e9956b 100644
--- a/tactics/btermdn.ml
+++ b/tactics/btermdn.ml
@@ -186,7 +186,5 @@ struct
(fun dn t ->
Dn.lookup dn (bounded_constr_val_discr_st env sigma st) (t,!dnet_depth))
- let app f dn = Dn.app f dn
-
end
diff --git a/tactics/btermdn.mli b/tactics/btermdn.mli
index ab201a1872..01d68a8045 100644
--- a/tactics/btermdn.mli
+++ b/tactics/btermdn.mli
@@ -38,7 +38,6 @@ sig
val rmv : t -> pattern -> Z.t -> t
val lookup : Environ.env -> Evd.evar_map -> TransparentState.t option -> t -> EConstr.constr -> Z.t list
- val app : (Z.t -> unit) -> t -> unit
end
val dnet_depth : int ref
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 96cbbf0ba8..b4d7e7d7f0 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -158,7 +158,7 @@ let unify_resolve ~with_evars flags h diff = match diff with
| None ->
Hints.hint_res_pf ~with_evars ~with_classes:false ~flags h
| Some (diff, ty) ->
- let () = assert (not h.hint_poly) in
+ let () = assert (Option.is_empty h.hint_uctx) in
Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Tacmach.New.project gl in
@@ -203,11 +203,10 @@ let unify_resolve_refine flags h diff =
let with_prods nprods h f =
if get_typeclasses_limit_intros () then
Proofview.Goal.enter begin fun gl ->
- let { hint_term = c; hint_poly = poly } = h in
- if poly || Int.equal nprods 0 then f None
+ if Option.has_some h.hint_uctx || Int.equal nprods 0 then f None
else
let sigma = Tacmach.New.project gl in
- let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma c in
+ let ty = Retyping.get_type_of (Proofview.Goal.env gl) sigma h.hint_term in
let diff = nb_prod sigma ty - nprods in
if (>=) diff 0 then f (Some (diff, ty))
else Tacticals.New.tclZEROMSG (str"Not enough premisses")
@@ -489,12 +488,12 @@ let make_resolve_hyp env sigma st only_classes pri decl =
let hints = build_subclasses ~check:false env sigma id empty_hint_info in
(List.map_append
(fun (path,info,c) ->
- let h = IsConstr (EConstr.of_constr c,Univ.ContextSet.empty) [@ocaml.warning "-3"] in
- make_resolves env sigma ~name:(PathHints path) info ~check:true ~poly:false h)
+ let h = IsConstr (EConstr.of_constr c, None) [@ocaml.warning "-3"] in
+ make_resolves env sigma ~name:(PathHints path) info ~check:true h)
hints)
else []
in
- (hints @ make_resolves env sigma pri ~name ~check:false ~poly:false (IsGlobRef id))
+ (hints @ make_resolves env sigma pri ~name ~check:false (IsGlobRef id))
else []
let make_hints g (modes,st) only_classes sign =
diff --git a/tactics/dn.ml b/tactics/dn.ml
index 07eb49442a..c587f91e54 100644
--- a/tactics/dn.ml
+++ b/tactics/dn.ml
@@ -62,10 +62,10 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
pathrec []
let tm_of tm lbl =
- try [Trie.next tm lbl, true] with Not_found -> []
+ try [Trie.next tm lbl] with Not_found -> []
let rec skip_arg n tm =
- if Int.equal n 0 then [tm, true]
+ if Int.equal n 0 then [tm]
else
let labels = Trie.labels tm in
let map lbl = match lbl with
@@ -73,23 +73,19 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
| Some (_, m) ->
skip_arg (pred n + m) (Trie.next tm lbl)
in
- List.flatten (List.map map labels)
+ List.map_append map labels
let lookup tm dna t =
let rec lookrec t tm =
match dna t with
| Nothing -> tm_of tm None
| Label(lbl,v) ->
- tm_of tm None@
- (List.fold_left
- (fun l c ->
- List.flatten(List.map (fun (tm, b) ->
- if b then lookrec c tm
- else [tm,b]) l))
- (tm_of tm (Some(lbl,List.length v))) v)
+ let fold accu c = List.map_append (fun tm -> lookrec c tm) accu in
+ tm_of tm None @
+ (List.fold_left fold (tm_of tm (Some (lbl, List.length v))) v)
| Everything -> skip_arg 1 tm
in
- List.flatten (List.map (fun (tm,b) -> ZSet.elements (Trie.get tm)) (lookrec t tm))
+ List.map_append (fun tm -> ZSet.elements (Trie.get tm)) (lookrec t tm)
let pattern dna pat = path_of dna pat
@@ -99,7 +95,5 @@ prefix ordering, [dna] is the function returning the main node of a pattern *)
let rmv tm p inf =
Trie.remove p (ZSet.singleton inf) tm
- let app f tm = Trie.iter (fun _ p -> ZSet.iter f p) tm
-
end
diff --git a/tactics/dn.mli b/tactics/dn.mli
index 287aa2b257..85f9ef6dfb 100644
--- a/tactics/dn.mli
+++ b/tactics/dn.mli
@@ -38,6 +38,4 @@ sig
val lookup : t -> 'term lookup_fun -> 'term
-> Z.t list
- val app : (Z.t -> unit) -> t -> unit
-
end
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8478c1957a..60e2db4dce 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -659,8 +659,12 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
| None ->
tclFAIL 0 (str"Terms do not have convertible types")
| Some evd ->
- let e = lib_ref "core.eq.type" in
- let sym = lib_ref "core.eq.sym" in
+ let e,sym =
+ try lib_ref "core.eq.type", lib_ref "core.eq.sym"
+ with UserError _ ->
+ try lib_ref "core.identity.type", lib_ref "core.identity.sym"
+ with UserError _ ->
+ user_err (strbrk "Need a registration for either core.eq.type and core.eq.sym or core.identity.type and core.identity.sym.") in
Tacticals.New.pf_constr_of_global sym >>= fun sym ->
Tacticals.New.pf_constr_of_global e >>= fun e ->
let eq = applist (e, [t1;c1;c2]) in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 355cea8fa8..fe3efef7c5 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -129,22 +129,20 @@ type hints_path = GlobRef.t hints_path_gen
type hint_term =
| IsGlobRef of GlobRef.t
- | IsConstr of constr * Univ.ContextSet.t
+ | IsConstr of constr * Univ.ContextSet.t option (* None if monomorphic *)
type 'a with_uid = {
obj : 'a;
uid : KerName.t;
}
-type raw_hint = constr * types * Univ.ContextSet.t * bool (* poly *)
+type raw_hint = constr * types * Univ.ContextSet.t option
type hint = {
hint_term : constr;
hint_type : types;
- hint_uctx : Univ.ContextSet.t;
+ hint_uctx : Univ.ContextSet.t option; (* None if monomorphic *)
hint_clnv : clausenv;
- hint_poly : bool;
- (** Is the hint polymorpic and hence should be refreshed at each application *)
}
type 'a with_metadata =
@@ -334,15 +332,19 @@ let strip_params env sigma c =
| _ -> c)
| _ -> c
+let merge_context_set_opt sigma ctx = match ctx with
+| None -> sigma
+| Some ctx -> Evd.merge_context_set Evd.univ_flexible sigma ctx
+
let instantiate_hint env sigma p =
- let mk_clenv (c, cty, ctx, poly) =
- let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+ let mk_clenv (c, cty, ctx) =
+ let sigma = merge_context_set_opt sigma ctx in
let cl = mk_clenv_from_env env sigma None (c,cty) in
let cl = {cl with templval =
{ cl.templval with rebus = strip_params env sigma cl.templval.rebus };
env = empty_env}
in
- { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; hint_poly = poly }
+ { hint_term = c; hint_type = cty; hint_uctx = ctx; hint_clnv = cl; }
in
let code = match p.code.obj with
| Res_pf c -> Res_pf (mk_clenv c)
@@ -816,7 +818,7 @@ let secvars_of_constr env sigma c =
let secvars_of_global env gr =
secvars_of_idset (vars_of_global env gr)
-let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
+let make_exact_entry env sigma info ?(name=PathAny) (c, cty, ctx) =
let secvars = secvars_of_constr env sigma c in
let cty = strip_outer_cast sigma cty in
match EConstr.kind sigma cty with
@@ -835,13 +837,13 @@ let make_exact_entry env sigma info ~poly ?(name=PathAny) (c, cty, ctx) =
(Some hd,
{ pri; pat = Some pat; name;
db = None; secvars;
- code = with_uid (Give_exact (c, cty, ctx, poly)); })
+ code = with_uid (Give_exact (c, cty, ctx)); })
-let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) =
+let make_apply_entry env sigma hnf info ?(name=PathAny) (c, cty, ctx) =
let cty = if hnf then hnf_constr env sigma cty else cty in
match EConstr.kind sigma cty with
| Prod _ ->
- let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
+ let sigma' = merge_context_set_opt sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
let hd =
@@ -861,49 +863,27 @@ let make_apply_entry env sigma hnf info ~poly ?(name=PathAny) (c, cty, ctx) =
{ pri; pat = Some pat; name;
db = None;
secvars;
- code = with_uid (Res_pf(c,cty,ctx,poly)); })
+ code = with_uid (Res_pf(c,cty,ctx)); })
else
(Some hd,
{ pri; pat = Some pat; name;
db = None; secvars;
- code = with_uid (ERes_pf(c,cty,ctx,poly)); })
+ code = with_uid (ERes_pf(c,cty,ctx)); })
| _ -> failwith "make_apply_entry"
(* flags is (e,h,v) with e=true if eapply and h=true if hnf and v=true if verbose
c is a constr
cty is the type of constr *)
-let pr_hint_term env sigma ctx = function
- | IsGlobRef gr -> pr_global gr
- | IsConstr (c, ctx) ->
- let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- pr_econstr_env env sigma c
-
-let warn_polymorphic_hint =
- CWarnings.create ~name:"polymorphic-hint" ~category:"automation"
- (fun hint -> strbrk"Using polymorphic hint " ++ hint ++
- str" monomorphically" ++
- strbrk" use Polymorphic Hint to use it polymorphically.")
-
-let fresh_global_or_constr env sigma poly cr =
- let isgr, (c, ctx) =
- match cr with
- | IsGlobRef gr ->
- let (c, ctx) = UnivGen.fresh_global_instance env gr in
- true, (EConstr.of_constr c, ctx)
- | IsConstr (c, ctx) -> false, (c, ctx)
- in
- if poly then (c, ctx)
- else if Univ.ContextSet.is_empty ctx then (c, ctx)
- else begin
- if isgr then
- warn_polymorphic_hint (pr_hint_term env sigma ctx cr);
- DeclareUctx.declare_universe_context ~poly:false ctx;
- (c, Univ.ContextSet.empty)
- end
-
-let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr =
- let c, ctx = fresh_global_or_constr env sigma poly cr in
+let fresh_global_or_constr env sigma cr = match cr with
+| IsGlobRef gr ->
+ let (c, ctx) = UnivGen.fresh_global_instance env gr in
+ let ctx = if Environ.is_polymorphic env gr then Some ctx else None in
+ (EConstr.of_constr c, ctx)
+| IsConstr (c, ctx) -> (c, ctx)
+
+let make_resolves env sigma (eapply, hnf) info ~check ?name cr =
+ let c, ctx = fresh_global_or_constr env sigma cr in
let cty = Retyping.get_type_of env sigma c in
let try_apply f =
try
@@ -914,8 +894,8 @@ let make_resolves env sigma (eapply, hnf) info ~check ~poly ?name cr =
with Failure _ -> None
in
let ents = List.map_filter try_apply
- [make_exact_entry env sigma info ~poly ?name;
- make_apply_entry env sigma hnf info ~poly ?name]
+ [make_exact_entry env sigma info ?name;
+ make_apply_entry env sigma hnf info ?name]
in
if check && List.is_empty ents then
user_err ~hdr:"Hint"
@@ -929,9 +909,9 @@ let make_resolve_hyp env sigma decl =
let hname = NamedDecl.get_id decl in
let c = mkVar hname in
try
- [make_apply_entry env sigma true empty_hint_info ~poly:false
+ [make_apply_entry env sigma true empty_hint_info
~name:(PathHints [GlobRef.VarRef hname])
- (c, NamedDecl.get_type decl, Univ.ContextSet.empty)]
+ (c, NamedDecl.get_type decl, None)]
with
| Failure _ -> []
| e when noncritical e -> anomaly (Pp.str "make_resolve_hyp.")
@@ -977,9 +957,9 @@ let make_mode ref m =
str" arguments while the mode declares " ++ int (Array.length m'))
else m'
-let make_trivial env sigma poly ?(name=PathAny) r =
- let c,ctx = fresh_global_or_constr env sigma poly r in
- let sigma = Evd.merge_context_set univ_flexible sigma ctx in
+let make_trivial env sigma ?(name=PathAny) r =
+ let c,ctx = fresh_global_or_constr env sigma r in
+ let sigma = merge_context_set_opt sigma ctx in
let t = hnf_constr env sigma (Retyping.get_type_of env sigma c) in
let hd = head_constr sigma t in
let ce = mk_clenv_from_env env sigma None (c,t) in
@@ -989,7 +969,7 @@ let make_trivial env sigma poly ?(name=PathAny) r =
name = name;
db = None;
secvars = secvars_of_constr env sigma c;
- code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx,poly)) })
+ code= with_uid (Res_pf_THEN_trivial_fail(c,t,ctx)) })
@@ -1102,10 +1082,10 @@ let subst_autohint (subst, obj) =
with Bound -> gr')
in
let subst_mps subst c = EConstr.of_constr (subst_mps subst (EConstr.Unsafe.to_constr c)) in
- let subst_aux ((c, t, ctx, poly) as h) =
+ let subst_aux ((c, t, ctx) as h) =
let c' = subst_mps subst c in
let t' = subst_mps subst t in
- if c==c' && t'==t then h else (c', t', ctx, poly)
+ if c==c' && t'==t then h else (c', t', ctx)
in
let subst_hint (k,data as hint) =
let k' = Option.Smart.map subst_key k in
@@ -1214,13 +1194,13 @@ let add_resolves env sigma clist ~local ~superglobal dbnames =
List.iter
(fun dbname ->
let r =
- List.flatten (List.map (fun (pri, poly, hnf, path, gr) ->
+ List.flatten (List.map (fun (pri, hnf, path, gr) ->
make_resolves env sigma (true, hnf)
- pri ~check:true ~poly ~name:path gr) clist)
+ pri ~check:true ~name:path gr) clist)
in
let check (_, hint) = match hint.code.obj with
- | ERes_pf (c, cty, ctx, _) ->
- let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
+ | ERes_pf (c, cty, ctx) ->
+ let sigma' = merge_context_set_opt sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let miss = clenv_missing ce in
let nmiss = List.length miss in
@@ -1288,7 +1268,7 @@ let add_externs info tacast ~local ~superglobal dbnames =
let add_trivials env sigma l ~local ~superglobal dbnames =
List.iter
(fun dbname ->
- let l = List.map (fun (name, poly, c) -> make_trivial env sigma poly ~name c) l in
+ let l = List.map (fun (name, c) -> make_trivial env sigma ~name c) l in
let hint = make_hint ~local dbname (AddHints { superglobal; hints = l }) in
Lib.add_anonymous_leaf (inAutoHint hint))
dbnames
@@ -1298,8 +1278,8 @@ type hnf = bool
type nonrec hint_info = hint_info
type hints_entry =
- | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
- | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
+ | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
+ | HintsImmediateEntry of (hints_path_atom * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -1372,24 +1352,21 @@ let expand_constructor_hints env sigma lems =
match EConstr.kind sigma lem with
| Ind (ind,u) ->
List.init (nconstructors env ind)
- (fun i ->
- let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
- (Evd.universe_context_set sigma) in
- not (Univ.ContextSet.is_empty ctx),
- IsConstr (mkConstructU ((ind,i+1),u),ctx))
+ (fun i -> IsGlobRef (GlobRef.ConstructRef ((ind,i+1))))
| _ ->
let (c, ctx) = prepare_hint false env sigma (evd,lem) in
- [not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)]) lems
+ let ctx = if Univ.ContextSet.is_empty ctx then None else Some ctx in
+ [IsConstr (c, ctx)]) lems
(* builds a hint database from a constr signature *)
(* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
let constructor_hints env sigma eapply lems =
let lems = expand_constructor_hints env sigma lems in
- List.map_append (fun (poly, lem) ->
- make_resolves env sigma (eapply, true) empty_hint_info ~check:true ~poly lem) lems
+ List.map_append (fun lem ->
+ make_resolves env sigma (eapply, true) empty_hint_info ~check:true lem) lems
-let make_resolves env sigma info ~check ~poly ?name hint =
- make_resolves env sigma (true, false) info ~check ~poly ?name hint
+let make_resolves env sigma info ~check ?name hint =
+ make_resolves env sigma (true, false) info ~check ?name hint
let make_local_hint_db env sigma ts eapply lems =
let map c = c env sigma in
@@ -1650,7 +1627,8 @@ let connect_hint_clenv h gl =
let sigma = Tacmach.New.project gl in
let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
(* Still, we need to update the universes *)
- if h.hint_poly then
+ match h.hint_uctx with
+ | Some ctx ->
(* Refresh the instance of the hint *)
let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let emap c = Vars.subst_univs_level_constr subst c in
@@ -1662,21 +1640,19 @@ let connect_hint_clenv h gl =
evd = Evd.map_metas emap evd;
env = Proofview.Goal.env gl;
}
- else
- let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
+ | None ->
{ clenv with evd = evd ; env = Proofview.Goal.env gl }
let fresh_hint env sigma h =
let { hint_term = c; hint_uctx = ctx } = h in
- if h.hint_poly then
+ match h.hint_uctx with
+ | None -> sigma, c
+ | Some ctx ->
(* Refresh the instance of the hint *)
let (subst, ctx) = UnivGen.fresh_universe_context_set_instance ctx in
let c = Vars.subst_univs_level_constr subst c in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
sigma, c
- else
- let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
- sigma, c
let hint_res_pf ?with_evars ?with_classes ?flags h =
Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/hints.mli b/tactics/hints.mli
index e061bd7648..dd22cff10b 100644
--- a/tactics/hints.mli
+++ b/tactics/hints.mli
@@ -42,9 +42,8 @@ type 'a hint_ast =
type hint = private {
hint_term : constr;
hint_type : types;
- hint_uctx : Univ.ContextSet.t;
+ hint_uctx : Univ.ContextSet.t option;
hint_clnv : clausenv;
- hint_poly : bool;
}
type 'a hints_path_atom_gen =
@@ -170,11 +169,11 @@ type hnf = bool
type hint_term =
| IsGlobRef of GlobRef.t
- | IsConstr of constr * Univ.ContextSet.t [@ocaml.deprecated "Declare a hint constant instead"]
+ | IsConstr of constr * Univ.ContextSet.t option [@ocaml.deprecated "Declare a hint constant instead"]
type hints_entry =
- | HintsResolveEntry of (hint_info * bool * hnf * hints_path_atom * hint_term) list
- | HintsImmediateEntry of (hints_path_atom * bool * hint_term) list
+ | HintsResolveEntry of (hint_info * hnf * hints_path_atom * hint_term) list
+ | HintsImmediateEntry of (hints_path_atom * hint_term) list
| HintsCutEntry of hints_path
| HintsUnfoldEntry of evaluable_global_reference list
| HintsTransparencyEntry of evaluable_global_reference hints_transparency_target * bool
@@ -211,7 +210,7 @@ val prepare_hint : bool (* Check no remaining evars *) ->
has missing arguments. *)
val make_resolves :
- env -> evar_map -> hint_info -> check:bool -> poly:bool -> ?name:hints_path_atom ->
+ env -> evar_map -> hint_info -> check:bool -> ?name:hints_path_atom ->
hint_term -> hint_entry list
(** [make_resolve_hyp hname htyp].
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 41899132a6..498a4cfc26 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -116,7 +116,11 @@ let make_inv_predicate env evd indf realargs id status concl =
(* Now, we can recurse down this list, for each ai,(mkRel k) whether to
push <Ai>(mkRel k)=ai (when Ai is closed).
In any case, we carry along the rest of pairs *)
- let eqdata = Coqlib.build_coq_eq_data () in
+ let eqdata =
+ try Coqlib.build_coq_eq_data ()
+ with UserError _ ->
+ try Coqlib.build_coq_identity_data ()
+ with UserError _ -> user_err (str "No registered equality.") in
let rec build_concl eqns args n = function
| [] -> it_mkProd concl eqns, Array.rev_of_list args
| ai :: restlist ->
@@ -351,8 +355,12 @@ let remember_first_eq id x = if !x == Logic.MoveLast then x := Logic.MoveAfter i
let dest_nf_eq env sigma t = match EConstr.kind sigma t with
| App (r, [| t; x; y |]) ->
let open Reductionops in
- let eq = Coqlib.lib_ref "core.eq.type" in
- if isRefX sigma eq r then
+ let is_global_exists gr c =
+ Coqlib.has_ref gr && isRefX sigma (Coqlib.lib_ref gr) c
+ in
+ let is_eq = is_global_exists "core.eq.type" r in
+ let is_identity = is_global_exists "core.identity.type" r in
+ if is_eq || is_identity then
(t, whd_all env sigma x, whd_all env sigma y)
else user_err Pp.(str "Not an equality.")
| _ ->
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 23:26:36 +0000