diff options
| author | barras | 2009-12-01 22:31:59 +0000 |
|---|---|---|
| committer | barras | 2009-12-01 22:31:59 +0000 |
| commit | 3594d04da08dbeb58e29234dd33eaf6addc195d8 (patch) | |
| tree | 77f72f96070fbf00910764c1ef40b4e4b37e2c83 /plugins/interface/coqparser_plugin.mllib | |
| parent | 84b3ae516fffffc60989817eab9cf5749c2f492a (diff) | |
two improvements of the guard condition:
- a matched expression is reduced (in order to check if it's a subterm)
to hnf only when it contains variables that are subterms;
- a matched expression is checked to be a subterm only when it belongs to
a *recursive* type.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12553 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/interface/coqparser_plugin.mllib')
0 files changed, 0 insertions, 0 deletions