diff options
| author | barras | 2005-06-06 20:08:18 +0000 |
|---|---|---|
| committer | barras | 2005-06-06 20:08:18 +0000 |
| commit | 76dbe6adab29ea6950955c42415cb0b22c15adbe (patch) | |
| tree | 3265ca5beb4cdab102a61e4abe050549c64bcac4 /pretyping/evarconv.ml | |
| parent | 82b053c589fe74359e009e8216970b170be4383d (diff) | |
essai de typage des instantiations d\'evars
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7117 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarconv.ml')
| -rw-r--r-- | pretyping/evarconv.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml index 4af5a43cf8..047b306ed6 100644 --- a/pretyping/evarconv.ml +++ b/pretyping/evarconv.ml @@ -177,8 +177,9 @@ let rec evar_conv_x env isevars pbty term1 term2 = true else *) - (* Maybe convertible but since reducing can erase evars which [evar_apprec]*) - (* could have found, we do it only if the terms are free of evar *) + (* Maybe convertible but since reducing can erase evars which [evar_apprec] + could have found, we do it only if the terms are free of evar. + Note: incomplete heuristic... *) if (not (has_undefined_evars isevars term1) & not (has_undefined_evars isevars term2) & |