diff options
| author | Hugo Herbelin | 2017-01-22 15:05:08 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2017-01-22 15:05:08 +0100 |
| commit | d6bcc6ebe4f65d0555414851f7e4fb6fa1fb22a4 (patch) | |
| tree | d8617530b9cd67aafaf7674dcf2ed42c3265a433 /pretyping | |
| parent | f22969902223ab54f56f25583b24dc27c4cd6f4e (diff) | |
Adding a new evar source to remember the name of evars which were
named in the original term.
Useful at least for debugging, useful to give a better message than
"this placeholder", even if in the loc is known in this case.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index 4684469826..95341307a3 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -275,9 +275,9 @@ let rec find_row_ind = function let inductive_template evdref env tmloc ind = let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in let arsign = inductive_alldecls_env env indu in - let hole_source = match tmloc with - | Some loc -> fun i -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) - | None -> fun _ -> (Loc.ghost, Evar_kinds.InternalHole) in + let hole_source i = match tmloc with + | Some loc -> (loc, Evar_kinds.TomatchTypeParameter (ind,i)) + | None -> (Loc.ghost, Evar_kinds.TomatchTypeParameter (ind,i)) in let (_,evarl,_) = List.fold_right (fun decl (subst,evarl,n) -> |