diff options
| author | herbelin | 2009-08-03 20:50:11 +0000 |
|---|---|---|
| committer | herbelin | 2009-08-03 20:50:11 +0000 |
| commit | f9f35dc36f5249a2de18005ab59ae934e0fa7075 (patch) | |
| tree | 4d3dd839db319df1945c8fef474284e6f4e5f3e3 /ide | |
| parent | 25dde2366a4db47e5da13b2bbe4d03a31235706f (diff) | |
Added "etransitivity".
Added support for "injection" and "discriminate" on JMeq.
Seized the opportunity to update coqlib.ml and to rely more on it for
finding the equality lemmas.
Fixed typos in coqcompat.ml.
Propagated symmetry convert_concl fix to transitivity (see 11521).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12259 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/coq.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ide/coq.ml b/ide/coq.ml index d81bb42f24..35feb59edf 100644 --- a/ide/coq.ml +++ b/ide/coq.ml @@ -523,14 +523,14 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = pr_ast ^".") ] @ - (if is_equation ast then + (if is_equality_type ast then [ "discriminate "^ident, "discriminate "^ident^"."; "injection "^ident, "injection "^ident^"." ] else []) @ (let _,t = splay_prod env sigma ast in - if is_equation t then + if is_equality_type t then [ "rewrite "^ident, "rewrite "^ident^"."; "rewrite <- "^ident, "rewrite <- "^ident^"." ] else @@ -546,7 +546,7 @@ let hyp_menu (env, sigma, ((coqident,ident),_,ast),(s,pr_ast)) = ("inversion_clear "^ident^".")] let concl_menu (_,_,concl,_) = - let is_eq = is_equation concl in + let is_eq = is_equality_type concl in ["intro", "intro."; "intros", "intros."; "intuition","intuition." ] @ |