diff options
author | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2010-10-14 17:51:11 +0200 |
commit | 3e96002677226c0cdaa8f355938a76cfb37a722a (patch) | |
tree | 3ca96e142fdb68e464d2f5f403f315282b94f922 /tactics/extratactics.ml4 | |
parent | f18e6146f4fd6ed5b8ded10a3e602f5f64f919f4 (diff) |
Imported Upstream version 8.3upstream/8.3
Diffstat (limited to 'tactics/extratactics.ml4')
-rw-r--r-- | tactics/extratactics.ml4 | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4 index e1ac42c2..3f069ab2 100644 --- a/tactics/extratactics.ml4 +++ b/tactics/extratactics.ml4 @@ -8,7 +8,7 @@ (*i camlp4deps: "parsing/grammar.cma" i*) -(* $Id: extratactics.ml4 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: extratactics.ml4 13434 2010-09-18 20:11:37Z msozeau $ *) open Pp open Pcoq @@ -624,3 +624,8 @@ TACTIC EXTEND hget_evar END (**********************************************************************) + +TACTIC EXTEND constr_eq +| [ "constr_eq" constr(x) constr(y) ] -> [ + if eq_constr x y then tclIDTAC else tclFAIL 0 (str "Not equal") ] +END |