diff options
| author | Matthieu Sozeau | 2014-09-24 11:11:28 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2014-09-24 21:05:06 +0200 |
| commit | 31e4222d35b614efa94a1d68b5d6491ea9e46bfa (patch) | |
| tree | f5b60f2a6ab94ad7f8ef6a0c9094804f204140be | |
| parent | c955779074833066e9db81c9fb1b32493cfebfa2 (diff) | |
Return a Prop not an arbitrary Type, and correct a typo.
| -rw-r--r-- | pretyping/tacred.ml | 2 | ||||
| -rw-r--r-- | theories/Logic/EqdepFacts.v | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 67aef0cfcd..0088563fab 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 diff --git a/theories/Logic/EqdepFacts.v b/theories/Logic/EqdepFacts.v index 58b6d076c5..afd0ecf046 100644 --- a/theories/Logic/EqdepFacts.v +++ b/theories/Logic/EqdepFacts.v @@ -376,7 +376,7 @@ Proof. (eq_sym (UIP (eq_refl x) (eq_refl x)))). - destruct z. unfold e. destruct (UIP _ _). reflexivity. - change - (match eq_refl x as y' in _ = x' return y' = y' -> Type with + (match eq_refl x as y' in _ = x' return y' = y' -> Prop with | eq_refl => fun z => z = (eq_refl (eq_refl x)) end (eq_trans (eq_trans (UIP (eq_refl x) (eq_refl x)) z) (eq_sym (UIP (eq_refl x) (eq_refl x))))). |