Skip to content

Commit

Permalink
[econstr] Forbid calling to_constr in open terms.
Browse files Browse the repository at this point in the history
We forbid calling `EConstr.to_constr` on terms that are not evar-free,
as to progress towards enforcing the invariant that `Constr.t` is
evar-free. [c.f. #6308]

Due to compatibility constraints we provide an optional parameter to
`to_constr`, `abort` which can be used to overcome this restriction
until we fix all parts of the code.

Now, grepping for `~abort:false` should return the questionable
parts of the system.

Not a lot of places had to be fixed, some comments:

- problems with the interface due to `Evd/Constr` [`Evd.define` being
  the prime example] do seem real!
- inductives also look bad with regards to `Constr/EConstr`.
- code in plugins needs work.

A notable user of this "feature" is `Obligations/Program` that seem to
like to generate kernel-level entries with free evars, then to scan
them and workaround this problem by generating constants.
ejgallego committed Mar 31, 2018
1 parent 2d2d164 commit 9f723f1
Showing 23 changed files with 69 additions and 46 deletions.
8 changes: 8 additions & 0 deletions dev/ci/user-overlays/06454-ejgallego-evar+strict_to_constr.sh
Original file line number Diff line number Diff line change
@@ -0,0 +1,8 @@
if [ "$CI_PULL_REQUEST" = "6454" ] || [ "$CI_BRANCH" = "evar+strict_to_constr" ]; then

# ltac2_CI_BRANCH=econstr+more_fix
# ltac2_CI_GITURL=https://github.com/ejgallego/ltac2

Equations_CI_BRANCH=evar+strict_to_constr
Equations_CI_GITURL=https://github.com/ejgallego/Coq-Equations
fi
16 changes: 11 additions & 5 deletions engine/eConstr.ml
Original file line number Diff line number Diff line change
@@ -40,7 +40,7 @@ val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type
val whd_evar : Evd.evar_map -> t -> t
val of_kind : (t, t, ESorts.t, EInstance.t) Constr.kind_of_term -> t
val of_constr : Constr.t -> t
val to_constr : evar_map -> t -> Constr.t
val to_constr : ?abort_on_undefined_evars:bool -> evar_map -> t -> Constr.t
val unsafe_to_constr : t -> Constr.t
val unsafe_eq : (t, Constr.t) eq
val of_named_decl : (Constr.t, Constr.types) Context.Named.Declaration.pt -> (t, t) Context.Named.Declaration.pt
@@ -110,11 +110,16 @@ let of_constr c = c
let unsafe_to_constr c = c
let unsafe_eq = Refl

let rec to_constr sigma c = match Constr.kind c with
let to_constr ?(abort_on_undefined_evars=true) sigma c =
let rec to_constr c = match Constr.kind c with
| Evar ev ->
begin match safe_evar_value sigma ev with
| Some c -> to_constr sigma c
| None -> Constr.map (fun c -> to_constr sigma c) c
| Some c -> to_constr c
| None ->
if abort_on_undefined_evars then
anomaly ~label:"econstr" Pp.(str "grounding a non evar-free term")
else
Constr.map (fun c -> to_constr c) c
end
| Sort (Sorts.Type u) ->
let u' = Evd.normalize_universe sigma u in
@@ -128,7 +133,8 @@ let rec to_constr sigma c = match Constr.kind c with
| Construct (co, u) when not (Univ.Instance.is_empty u) ->
let u' = Evd.normalize_universe_instance sigma u in
if u' == u then c else mkConstructU (co, u')
| _ -> Constr.map (fun c -> to_constr sigma c) c
| _ -> Constr.map (fun c -> to_constr c) c
in to_constr c

let of_named_decl d = d
let unsafe_to_named_decl d = d
13 changes: 8 additions & 5 deletions engine/eConstr.mli
Original file line number Diff line number Diff line change
@@ -68,11 +68,14 @@ val kind : Evd.evar_map -> t -> (t, t, ESorts.t, EInstance.t) Constr.kind_of_ter

val kind_upto : Evd.evar_map -> Constr.t -> (Constr.t, Constr.t, Sorts.t, Univ.Instance.t) Constr.kind_of_term

val to_constr : Evd.evar_map -> t -> Constr.t
(** Returns the evar-normal form of the argument, and cast it as a theoretically
evar-free term. In practice this function does not check that the result
is actually evar-free, it is currently the duty of the caller to do so.
This might change in the future. *)
val to_constr : ?abort_on_undefined_evars:bool -> Evd.evar_map -> t -> Constr.t
(** Returns the evar-normal form of the argument. Note that this
function is supposed to be called when the original term has not
more free-evars anymore. If you need compatibility with the old
semantics, set [abort_on_undefined_evars] to [false].
For getting the evar-normal form of a term with evars see
{!Evarutil.nf_evar}. *)

val kind_of_type : Evd.evar_map -> t -> (t, t) Term.kind_of_type

4 changes: 2 additions & 2 deletions engine/evarutil.ml
Original file line number Diff line number Diff line change
@@ -72,9 +72,9 @@ let flush_and_check_evars sigma c =
(** Term exploration up to instantiation. *)
let kind_of_term_upto = EConstr.kind_upto

let nf_evar0 sigma t = EConstr.to_constr sigma (EConstr.of_constr t)
let nf_evar0 sigma t = EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
let whd_evar = EConstr.whd_evar
let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr sigma c)
let nf_evar sigma c = EConstr.of_constr (EConstr.to_constr ~abort_on_undefined_evars:false sigma c)

let j_nf_evar sigma j =
{ uj_val = nf_evar sigma j.uj_val;
2 changes: 1 addition & 1 deletion plugins/cc/cctac.ml
Original file line number Diff line number Diff line change
@@ -90,7 +90,7 @@ let rec decompose_term env sigma t=
decompose_term env sigma c
| _ ->
let t = Termops.strip_outer_cast sigma t in
if closed0 sigma t then Symb (EConstr.to_constr sigma t) else raise Not_found
if closed0 sigma t then Symb (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) else raise Not_found

(* decompose equality in members and type *)
open Termops
6 changes: 3 additions & 3 deletions plugins/firstorder/sequent.ml
Original file line number Diff line number Diff line change
@@ -77,14 +77,14 @@ module CM=Map.Make(Constr)
module History=Set.Make(Hitem)

let cm_add sigma typ nam cm=
let typ = EConstr.to_constr sigma typ in
let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
try
let l=CM.find typ cm in CM.add typ (nam::l) cm
with
Not_found->CM.add typ [nam] cm

let cm_remove sigma typ nam cm=
let typ = EConstr.to_constr sigma typ in
let typ = EConstr.to_constr ~abort_on_undefined_evars:false sigma typ in
try
let l=CM.find typ cm in
let l0=List.filter (fun id-> not (Globnames.eq_gr id nam)) l in
@@ -152,7 +152,7 @@ let re_add_formula_list sigma lf seq=
redexes=List.fold_right HP.add lf seq.redexes;
context=List.fold_right do_one lf seq.context}

let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr sigma t) seq.context)
let find_left sigma t seq=List.hd (CM.find (EConstr.to_constr ~abort_on_undefined_evars:false sigma t) seq.context)

(*let rev_left seq=
try
2 changes: 1 addition & 1 deletion plugins/ssr/ssrcommon.ml
Original file line number Diff line number Diff line change
@@ -504,7 +504,7 @@ let nf_evar sigma t =
EConstr.Unsafe.to_constr (Evarutil.nf_evar sigma (EConstr.of_constr t))

let pf_abs_evars2 gl rigid (sigma, c0) =
let c0 = EConstr.to_constr sigma c0 in
let c0 = EConstr.to_constr ~abort_on_undefined_evars:false sigma c0 in
let sigma0, ucst = project gl, Evd.evar_universe_context sigma in
let nenv = env_size (pf_env gl) in
let abs_evar n k =
11 changes: 7 additions & 4 deletions plugins/ssr/ssrequality.ml
Original file line number Diff line number Diff line change
@@ -276,7 +276,7 @@ let unfoldintac occ rdx t (kt,_) gl =
let foldtac occ rdx ft gl =
let sigma0, concl0, env0 = project gl, pf_concl gl, pf_env gl in
let sigma, t = ft in
let t = EConstr.to_constr sigma t in
let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
let fold, conclude = match rdx with
| Some (_, (In_T _ | In_X_In_T _)) | None ->
let ise = Evd.create_evar_defs sigma in
@@ -557,7 +557,7 @@ let rwrxtac occ rdx_pat dir rule gl =
let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
let sigma, pat =
let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
mk_tpattern env sigma0 (sigma, EConstr.to_constr ~abort_on_undefined_evars:false sigma r) (rw_progress rhs) d (EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in
sigma, pats @ [pat] in
let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
let find_R, end_R = mk_tpattern_matcher sigma0 occ ~upats_origin rpats in
@@ -567,7 +567,7 @@ let rwrxtac occ rdx_pat dir rule gl =
let r = ref None in
(fun env c _ h -> do_once r (fun () -> find_rule (EConstr.of_constr c), c); mkRel h),
(fun concl -> closed0_check concl e gl;
let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ev c)) , x) in
let (d,(ev,ctx,c)) , x = assert_done r in (d,(ev,ctx, EConstr.to_constr ~abort_on_undefined_evars:false ev c)) , x) in
let concl0 = EConstr.Unsafe.to_constr concl0 in
let concl = eval_pattern env0 sigma0 concl0 rdx_pat occ find_R in
let (d, r), rdx = conclude concl in
@@ -589,7 +589,10 @@ let ssrinstancesofrule ist dir arg gl =
let rpat env sigma0 (sigma, pats) (d, r, lhs, rhs) =
let sigma, pat =
let rw_progress rhs t evd = rw_progress rhs (EConstr.of_constr t) evd in
mk_tpattern env sigma0 (sigma,EConstr.to_constr sigma r) (rw_progress rhs) d (EConstr.to_constr sigma lhs) in
mk_tpattern env sigma0
(sigma,EConstr.to_constr ~abort_on_undefined_evars:false sigma r)
(rw_progress rhs) d
(EConstr.to_constr ~abort_on_undefined_evars:false sigma lhs) in
sigma, pats @ [pat] in
let rpats = List.fold_left (rpat env0 sigma0) (r_sigma,[]) rules in
mk_tpattern_matcher ~all_instances:true ~raise_NoMatch:true sigma0 None ~upats_origin rpats in
2 changes: 1 addition & 1 deletion plugins/ssr/ssripats.ml
Original file line number Diff line number Diff line change
@@ -410,7 +410,7 @@ let tclLAST_GEN ~to_ind ((oclr, occ), t) conclusion = tclINDEPENDENTL begin
Goal.enter_one begin fun g ->
let pat = Ssrmatching.interp_cpattern sigma0 t None in
let cl0, env, sigma, hyps = Goal.(concl g, env g, sigma g, hyps g) in
let cl = EConstr.to_constr sigma cl0 in
let cl = EConstr.to_constr ~abort_on_undefined_evars:false sigma cl0 in
let (c, ucst), cl =
try Ssrmatching.fill_occ_pattern ~raise_NoMatch:true env sigma cl pat occ 1
with Ssrmatching.NoMatch -> Ssrmatching.redex_of_pattern env pat, cl in
2 changes: 1 addition & 1 deletion plugins/ssr/ssrview.ml
Original file line number Diff line number Diff line change
@@ -254,7 +254,7 @@ let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
let env = Goal.env g in
let sigma = Goal.sigma g in
let evars_of_p = Evd.evars_of_term (EConstr.to_constr sigma p) in
let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
let filter x _ = Evar.Set.mem x evars_of_p in
let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
let p = Reductionops.nf_evar sigma p in
3 changes: 2 additions & 1 deletion pretyping/cases.ml
Original file line number Diff line number Diff line change
@@ -2581,7 +2581,8 @@ let compile_program_cases ?loc style (typing_function, evdref) tycon env lvar
let body = it_mkLambda_or_LetIn (applist (j.uj_val, args)) lets in
let j =
{ uj_val = it_mkLambda_or_LetIn body tomatchs_lets;
uj_type = EConstr.of_constr (EConstr.to_constr !evdref tycon); }
(* XXX: is this normalization needed? *)
uj_type = Evarutil.nf_evar !evdref tycon; }
in j

(**************************************************************************)
4 changes: 2 additions & 2 deletions pretyping/evarsolve.ml
Original file line number Diff line number Diff line change
@@ -1592,14 +1592,14 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
Id.Set.subset (collect_vars evd rhs) !names
in
let body =
if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *)
if fast rhs then nf_evar evd rhs (** FIXME? *)
else
let t' = imitate (env,0) rhs in
if !progress then
(recheck_applications conv_algo (evar_env evi) evdref t'; t')
else t'
in (!evdref,body)

(* [define] tries to solve the problem "?ev[args] = rhs" when "?ev" is
* an (uninstantiated) evar such that "hyps |- ?ev : typ". Otherwise said,
* [define] tries to find an instance lhs such that
4 changes: 2 additions & 2 deletions pretyping/pretyping.ml
Original file line number Diff line number Diff line change
@@ -117,7 +117,7 @@ open ExtraEnv
exception Found of int array

let nf_fix sigma (nas, cs, ts) =
let inj c = EConstr.to_constr sigma c in
let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
(nas, Array.map inj cs, Array.map inj ts)

let search_guard ?loc env possible_indexes fixdefs =
@@ -1150,7 +1150,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match D
(* Correction of bug #5315 : we need to define an evar for *all* holes *)
let evkt = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s) in
let ev,_ = destEvar !evdref evkt in
evdref := Evd.define ev (to_constr !evdref v) !evdref;
evdref := Evd.define ev (to_constr ~abort_on_undefined_evars:false !evdref v) !evdref;
(* End of correction of bug #5315 *)
{ utj_val = v;
utj_type = s }
2 changes: 1 addition & 1 deletion pretyping/retyping.ml
Original file line number Diff line number Diff line change
@@ -170,7 +170,7 @@ let retype ?(polyprop=true) sigma =

and type_of_global_reference_knowing_parameters env c args =
let argtyps =
Array.map (fun c -> lazy (EConstr.to_constr sigma (type_of env c))) args in
Array.map (fun c -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma (type_of env c))) args in
match EConstr.kind sigma c with
| Ind (ind, u) ->
let u = EInstance.kind sigma u in
2 changes: 1 addition & 1 deletion pretyping/tacred.ml
Original file line number Diff line number Diff line change
@@ -558,7 +558,7 @@ let match_eval_ref_value env sigma constr stack =
else
None
| Proj (p, c) when not (Projection.unfolded p) ->
reduction_effect_hook env sigma (EConstr.to_constr sigma constr)
reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr)
(lazy (EConstr.to_constr sigma (applist (constr,stack))));
if is_evaluable env (EvalConstRef (Projection.constant p)) then
Some (mkProj (Projection.unfold p, c))
6 changes: 3 additions & 3 deletions pretyping/typing.ml
Original file line number Diff line number Diff line change
@@ -35,7 +35,7 @@ let meta_type evd mv =
let inductive_type_knowing_parameters env sigma (ind,u) jl =
let u = Unsafe.to_instance u in
let mspec = lookup_mind_specif env ind in
let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr sigma j.uj_type)) jl in
let paramstyp = Array.map (fun j -> lazy (EConstr.to_constr ~abort_on_undefined_evars:false sigma j.uj_type)) jl in
Inductive.type_of_inductive_knowing_parameters env (mspec,u) paramstyp

let e_type_judgment env evdref j =
@@ -155,7 +155,7 @@ let e_type_case_branches env evdref (ind,largs) pj c =
let p = pj.uj_val in
let params = List.map EConstr.Unsafe.to_constr params in
let () = e_is_correct_arity env evdref c pj ind specif params in
let lc = build_branches_type ind specif params (EConstr.to_constr !evdref p) in
let lc = build_branches_type ind specif params (EConstr.to_constr ~abort_on_undefined_evars:false !evdref p) in
let lc = Array.map EConstr.of_constr lc in
let n = (snd specif).Declarations.mind_nrealdecls in
let ty = whd_betaiota !evdref (lambda_applist_assum !evdref (n+1) p (realargs@[c])) in
@@ -207,7 +207,7 @@ let enrich_env env evdref =
Environ.env_of_pre_env penv'

let check_fix env sigma pfix =
let inj c = EConstr.to_constr sigma c in
let inj c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let (idx, (ids, cs, ts)) = pfix in
check_fix env (idx, (ids, Array.map inj cs, Array.map inj ts))

4 changes: 2 additions & 2 deletions pretyping/vnorm.ml
Original file line number Diff line number Diff line change
@@ -381,8 +381,8 @@ let cbv_vm env sigma c t =
if Termops.occur_meta sigma c then
CErrors.user_err Pp.(str "vm_compute does not support metas.");
(** This evar-normalizes terms beforehand *)
let c = EConstr.to_constr sigma c in
let t = EConstr.to_constr sigma t in
let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
let v = Vconv.val_of_constr env c in
EConstr.of_constr (nf_val env sigma v t)

4 changes: 2 additions & 2 deletions tactics/hints.ml
Original file line number Diff line number Diff line change
@@ -792,7 +792,7 @@ let make_exact_entry env sigma info poly ?(name=PathAny) (c, cty, ctx) =
match EConstr.kind sigma cty with
| Prod _ -> failwith "make_exact_entry"
| _ ->
let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr sigma cty) in
let pat = Patternops.pattern_of_constr env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma cty) in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_exact_entry"
@@ -814,7 +814,7 @@ let make_apply_entry env sigma (eapply,hnf,verbose) info poly ?(name=PathAny) (c
let sigma' = Evd.merge_context_set univ_flexible sigma ctx in
let ce = mk_clenv_from_env env sigma' None (c,cty) in
let c' = clenv_type (* ~reduce:false *) ce in
let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr sigma c') in
let pat = Patternops.pattern_of_constr env ce.evd (EConstr.to_constr ~abort_on_undefined_evars:false sigma c') in
let hd =
try head_pattern_bound pat
with BoundPattern -> failwith "make_apply_entry" in
2 changes: 1 addition & 1 deletion vernac/classes.ml
Original file line number Diff line number Diff line change
@@ -293,7 +293,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance)
(* Check that the type is free of evars now. *)
Pretyping.check_evars env Evd.empty sigma termtype;
let termtype = to_constr sigma termtype in
let term = Option.map (to_constr sigma) term in
let term = Option.map (to_constr ~abort_on_undefined_evars:false sigma) term in
if not (Evd.has_undefined sigma) && not (Option.is_empty term) then
declare_instance_constant k pri global imps ?hook id decl
poly sigma (Option.get term) termtype
4 changes: 2 additions & 2 deletions vernac/comDefinition.ml
Original file line number Diff line number Diff line change
@@ -88,8 +88,8 @@ let interp_definition pl bl poly red_option c ctypopt =
let evd = Evd.minimize_universes evd in
(* Substitute evars and universes, and add parameters.
Note: in program mode some evars may remain. *)
let ctx = List.map (EConstr.to_rel_decl evd) ctx in
let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr evd c) ctx in
let ctx = List.map Termops.(map_rel_decl (to_constr ~abort_on_undefined_evars:false evd)) ctx in
let c = Term.it_mkLambda_or_LetIn (EConstr.to_constr ~abort_on_undefined_evars:false evd c) ctx in
let tyopt = Option.map (fun ty -> Term.it_mkProd_or_LetIn (EConstr.to_constr evd ty) ctx) tyopt in
(* Keep only useful universes. *)
let uvars_fold uvars c =
3 changes: 2 additions & 1 deletion vernac/comFixpoint.ml
Original file line number Diff line number Diff line change
@@ -225,7 +225,8 @@ let interp_recursive ~program_mode ~cofix fixl notations =
(* Instantiate evars and check all are resolved *)
let sigma = solve_unif_constraints_with_heuristics env_rec sigma in
let sigma, _ = nf_evars_and_universes sigma in
let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr sigma) c) fixdefs in
(* XXX: We still have evars here in Program *)
let fixdefs = List.map (fun c -> Option.map EConstr.(to_constr ~abort_on_undefined_evars:false sigma) c) fixdefs in
let fixtypes = List.map EConstr.(to_constr sigma) fixtypes in
let fixctxs = List.map (fun (_,ctx) -> ctx) fixctxs in

8 changes: 5 additions & 3 deletions vernac/comProgramFixpoint.ml
Original file line number Diff line number Diff line change
@@ -229,7 +229,8 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
in
(* XXX: Capturing sigma here... bad bad *)
let hook = Lemmas.mk_hook (hook sigma) in
let fullcoqc = EConstr.to_constr sigma def in
(* XXX: Grounding non-ground terms here... bad bad *)
let fullcoqc = EConstr.to_constr ~abort_on_undefined_evars:false sigma def in
let fullctyp = EConstr.to_constr sigma typ in
Obligations.check_evars env sigma;
let evars, _, evars_def, evars_typ =
@@ -261,9 +262,10 @@ let do_program_recursive local poly fixkind fixl ntns =
let collect_evars id def typ imps =
(* Generalize by the recursive prototypes *)
let def =
EConstr.to_constr evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedLambda_or_LetIn (EConstr.of_constr def) rec_sign)
and typ =
EConstr.to_constr evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
(* Worrying... *)
EConstr.to_constr ~abort_on_undefined_evars:false evd (Termops.it_mkNamedProd_or_LetIn (EConstr.of_constr typ) rec_sign)
in
let evm = collect_evars_of_term evd def typ in
let evars, _, def, typ =
3 changes: 1 addition & 2 deletions vernac/himsg.ml
Original file line number Diff line number Diff line change
@@ -640,8 +640,7 @@ let explain_refiner_cannot_generalize env sigma ty =
pr_leconstr_env env sigma ty ++ str "."

let explain_no_occurrence_found env sigma c id =
let c = EConstr.to_constr sigma c in
str "Found no subterm matching " ++ pr_lconstr_env env sigma c ++
str "Found no subterm matching " ++ pr_leconstr_env env sigma c ++
str " in " ++
(match id with
| Some id -> Id.print id

0 comments on commit 9f723f1

Please sign in to comment.