diff options
| -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))))). |