aboutsummaryrefslogtreecommitdiff
path: root/pretyping/pretype_errors.ml
diff options
context:
space:
mode:
authorherbelin2011-03-05 16:42:21 +0000
committerherbelin2011-03-05 16:42:21 +0000
commit4e5c9882c74b04e69ef885db7c05ed31bf6a2732 (patch)
tree4e6f41225aab90a0a6c70172e56b36e0cd07a058 /pretyping/pretype_errors.ml
parent627a69094f6126aeb1d959b6f610e865ebde8a73 (diff)
Improved define_evar_as_lambda which was creating an unrelated new evar
for the domain instead of retrieving the known domain of the initial evar. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13881 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/pretype_errors.ml')
0 files changed, 0 insertions, 0 deletions