aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-27 15:33:11 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2018-02-27 15:33:11 +0100
commit52d90aee0859e5b67102435c6aee5c097c7ce4ce (patch)
tree3943603bfd0d7ab98206cdbd2b59372fe35876e3 /theories
parente3124e098ef8170dac2b348b91757a7034bc4999 (diff)
Add a comment on EConstr.to_constr regarding evar-freeness.
Diffstat (limited to 'theories')
0 files changed, 0 insertions, 0 deletions