diff options
| author |  Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 11:11:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <matthieu.sozeau@inria.fr> | 2014-09-24 21:05:06 +0200 |
| commit | 31e4222d35b614efa94a1d68b5d6491ea9e46bfa (patch) | |
| tree | f5b60f2a6ab94ad7f8ef6a0c9094804f204140be /pretyping/tacred.ml | |
| parent | c955779074833066e9db81c9fb1b32493cfebfa2 (diff) | |
Return a Prop not an arbitrary Type, and correct a typo.
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 67aef0cfc..0088563fa 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1071,7 +1071,7 @@ let is_projection env = function * Performs a betaiota reduction after unfolding. *) let unfoldoccs env sigma (occs,name) c = if is_projection env name then - error ("Cannot unfold primitie projection " ^ string_of_evaluable_ref env name) + error ("Cannot unfold primitive projection " ^ string_of_evaluable_ref env name) else let unfo nowhere_except_in locs = let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in |