diff options
Diffstat (limited to 'pretyping/pretype_errors.ml')
| -rw-r--r-- | pretyping/pretype_errors.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index b331574140..c0fa620485 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -183,7 +183,7 @@ let error_unexpected_type_loc loc env sigma actty expty = let error_not_product_loc loc env sigma c = raise_pretype_error (loc, env, sigma, NotProduct c) -(*s Error in conversion from AST to rawterms *) +(*s Error in conversion from AST to glob_constr *) let error_var_not_found_loc loc s = raise_pretype_error (loc, empty_env, Evd.empty, VarNotFound s) |