diff options
Diffstat (limited to 'pretyping/pretyping.ml')
| -rw-r--r-- | pretyping/pretyping.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 5a1a9df46..609567771 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -144,12 +144,15 @@ let transform_rec loc env sigma cl (ct,pt) = (***********************************************************************) +(* let ctxt_of_ids ids = Array.map (function | RRef (_,RVar id) -> VAR id | _ -> error "pretyping: arbitrary subst of ref not implemented") ids +*) +let ctxt_of_ids cl = cl let mt_evd = Evd.empty |