- Réintroduction d'un parseur de pattern (q_constr.ml4) à usage de

  la compilation de fichiers comme hipattern.ml (renommé en
  hipattern.ml4)
- Extension de eqdecide.ml4 pour qu'il gère les buts sans
  quantificateurs, basés soient sur sumbool soit sur or, et à symétrie
  près de la disjunction.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8652 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 316 insertions, 189 deletions

diff --git a/.depend b/.depend
index 063a49d9f..1401bebe7 100644
--- a/.depend
+++ b/.depend
@@ -427,7 +427,7 @@ contrib/first-order/unify.cmi: kernel/term.cmi
 contrib/funind/indfun_common.cmi: kernel/term.cmi pretyping/rawterm.cmi \
     lib/pp.cmi kernel/names.cmi library/libnames.cmi 
 contrib/funind/new_arg_principle.cmi: kernel/term.cmi proofs/tacmach.cmi \
-    kernel/names.cmi 
+    pretyping/rawterm.cmi kernel/names.cmi 
 contrib/funind/rawtermops.cmi: lib/util.cmi pretyping/rawterm.cmi \
     kernel/names.cmi library/libnames.cmi 
 contrib/funind/rawterm_to_relation.cmi: interp/topconstr.cmi \
@@ -1197,6 +1197,10 @@ parsing/printmod.cmo: lib/util.cmi lib/pp.cmi library/nametab.cmi \
 parsing/printmod.cmx: lib/util.cmx lib/pp.cmx library/nametab.cmx \
     kernel/names.cmx library/nameops.cmx library/libnames.cmx \
     library/global.cmx kernel/declarations.cmx parsing/printmod.cmi 
+parsing/q_constr.cmo: lib/util.cmi kernel/term.cmi pretyping/rawterm.cmi \
+    parsing/q_util.cmi pretyping/pattern.cmi kernel/names.cmi 
+parsing/q_constr.cmx: lib/util.cmx kernel/term.cmx pretyping/rawterm.cmx \
+    parsing/q_util.cmx pretyping/pattern.cmx kernel/names.cmx 
 parsing/q_coqast.cmo: lib/util.cmi interp/topconstr.cmi proofs/tacexpr.cmo \
     pretyping/rawterm.cmi parsing/q_util.cmi parsing/pcoq.cmi \
     kernel/names.cmi library/libnames.cmi interp/genarg.cmi 
@@ -1853,15 +1857,17 @@ tactics/hiddentac.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \
     tactics/evar_tactics.cmx tactics/hiddentac.cmi 
 tactics/hipattern.cmo: lib/util.cmi pretyping/termops.cmi kernel/term.cmi \
     tactics/tacticals.cmi proofs/tacmach.cmi pretyping/reductionops.cmi \
-    proofs/proof_trees.cmi lib/pp.cmi pretyping/pattern.cmi kernel/names.cmi \
-    library/nameops.cmi pretyping/matching.cmi pretyping/inductiveops.cmi \
+    pretyping/rawterm.cmi proofs/proof_trees.cmi lib/pp.cmi \
+    pretyping/pattern.cmi kernel/names.cmi library/nameops.cmi \
+    pretyping/matching.cmi library/libnames.cmi pretyping/inductiveops.cmi \
     library/global.cmi pretyping/evd.cmi kernel/environ.cmi \
     kernel/declarations.cmi interp/coqlib.cmi pretyping/clenv.cmi \
     tactics/hipattern.cmi 
 tactics/hipattern.cmx: lib/util.cmx pretyping/termops.cmx kernel/term.cmx \
     tactics/tacticals.cmx proofs/tacmach.cmx pretyping/reductionops.cmx \
-    proofs/proof_trees.cmx lib/pp.cmx pretyping/pattern.cmx kernel/names.cmx \
-    library/nameops.cmx pretyping/matching.cmx pretyping/inductiveops.cmx \
+    pretyping/rawterm.cmx proofs/proof_trees.cmx lib/pp.cmx \
+    pretyping/pattern.cmx kernel/names.cmx library/nameops.cmx \
+    pretyping/matching.cmx library/libnames.cmx pretyping/inductiveops.cmx \
     library/global.cmx pretyping/evd.cmx kernel/environ.cmx \
     kernel/declarations.cmx interp/coqlib.cmx pretyping/clenv.cmx \
     tactics/hipattern.cmi 
@@ -2812,25 +2818,23 @@ contrib/funind/indfun_common.cmx: lib/util.cmx pretyping/termops.cmx \
     kernel/declarations.cmx interp/coqlib.cmx \
     contrib/funind/indfun_common.cmi 
 contrib/funind/indfun_main.cmo: toplevel/vernacinterp.cmi lib/util.cmi \
-    pretyping/typing.cmi interp/topconstr.cmi kernel/term.cmi \
-    tactics/tactics.cmi tactics/tacticals.cmi tactics/tacinterp.cmi \
-    proofs/tacexpr.cmo proofs/refiner.cmi pretyping/rawterm.cmi \
-    parsing/pptactic.cmi lib/pp.cmi parsing/pcoq.cmi \
-    contrib/funind/new_arg_principle.cmi kernel/names.cmi library/nameops.cmi \
-    parsing/lexer.cmi contrib/funind/invfun.cmo pretyping/indrec.cmi \
-    contrib/funind/indfun_common.cmi contrib/funind/indfun.cmo \
-    library/global.cmi interp/genarg.cmi pretyping/evd.cmi \
-    parsing/egrammar.cmi toplevel/cerrors.cmi 
+    interp/topconstr.cmi kernel/term.cmi tactics/tactics.cmi \
+    tactics/tacticals.cmi tactics/tacinterp.cmi proofs/tacexpr.cmo \
+    proofs/refiner.cmi pretyping/rawterm.cmi parsing/pptactic.cmi lib/pp.cmi \
+    parsing/pcoq.cmi contrib/funind/new_arg_principle.cmi kernel/names.cmi \
+    library/nameops.cmi parsing/lexer.cmi contrib/funind/invfun.cmo \
+    pretyping/indrec.cmi contrib/funind/indfun_common.cmi \
+    contrib/funind/indfun.cmo interp/genarg.cmi parsing/egrammar.cmi \
+    toplevel/cerrors.cmi 
 contrib/funind/indfun_main.cmx: toplevel/vernacinterp.cmx lib/util.cmx \
-    pretyping/typing.cmx interp/topconstr.cmx kernel/term.cmx \
-    tactics/tactics.cmx tactics/tacticals.cmx tactics/tacinterp.cmx \
-    proofs/tacexpr.cmx proofs/refiner.cmx pretyping/rawterm.cmx \
-    parsing/pptactic.cmx lib/pp.cmx parsing/pcoq.cmx \
-    contrib/funind/new_arg_principle.cmx kernel/names.cmx library/nameops.cmx \
-    parsing/lexer.cmx contrib/funind/invfun.cmx pretyping/indrec.cmx \
-    contrib/funind/indfun_common.cmx contrib/funind/indfun.cmx \
-    library/global.cmx interp/genarg.cmx pretyping/evd.cmx \
-    parsing/egrammar.cmx toplevel/cerrors.cmx 
+    interp/topconstr.cmx kernel/term.cmx tactics/tactics.cmx \
+    tactics/tacticals.cmx tactics/tacinterp.cmx proofs/tacexpr.cmx \
+    proofs/refiner.cmx pretyping/rawterm.cmx parsing/pptactic.cmx lib/pp.cmx \
+    parsing/pcoq.cmx contrib/funind/new_arg_principle.cmx kernel/names.cmx \
+    library/nameops.cmx parsing/lexer.cmx contrib/funind/invfun.cmx \
+    pretyping/indrec.cmx contrib/funind/indfun_common.cmx \
+    contrib/funind/indfun.cmx interp/genarg.cmx parsing/egrammar.cmx \
+    toplevel/cerrors.cmx 
 contrib/funind/indfun.cmo: toplevel/vernacexpr.cmo lib/util.cmi \
     interp/topconstr.cmi kernel/term.cmi proofs/tacmach.cmi \
     library/states.cmi contrib/recdef/recdef.cmo \
@@ -2863,34 +2867,36 @@ contrib/funind/invfun.cmx: lib/util.cmx kernel/term.cmx tactics/tactics.cmx \
     tactics/extratactics.cmx tactics/equality.cmx kernel/declarations.cmx 
 contrib/funind/new_arg_principle.cmo: toplevel/vernacexpr.cmo \
     toplevel/vernacentries.cmi lib/util.cmi pretyping/unification.cmi \
-    pretyping/termops.cmi kernel/term.cmi tactics/tactics.cmi \
-    tactics/tacticals.cmi proofs/tactic_debug.cmi pretyping/tacred.cmi \
-    proofs/tacmach.cmi tactics/tacinterp.cmi pretyping/reductionops.cmi \
-    contrib/recdef/recdef.cmo pretyping/rawterm.cmi proofs/proof_type.cmi \
-    parsing/printer.cmi lib/pp.cmi proofs/pfedit.cmi lib/options.cmi \
-    kernel/names.cmi library/libnames.cmi pretyping/indrec.cmi \
-    contrib/funind/indfun_common.cmi tactics/hiddentac.cmi library/global.cmi \
-    interp/genarg.cmi pretyping/evd.cmi tactics/equality.cmi \
-    kernel/environ.cmi kernel/entries.cmi tactics/eauto.cmi \
-    library/declare.cmi kernel/declarations.cmi library/decl_kinds.cmo \
-    interp/coqlib.cmi toplevel/command.cmi kernel/closure.cmi \
-    pretyping/clenv.cmi toplevel/cerrors.cmi \
-    contrib/funind/new_arg_principle.cmi 
+    pretyping/typing.cmi pretyping/termops.cmi kernel/term.cmi \
+    tactics/tactics.cmi tactics/tacticals.cmi proofs/tactic_debug.cmi \
+    pretyping/tacred.cmi proofs/tacmach.cmi tactics/tacinterp.cmi \
+    pretyping/reductionops.cmi contrib/recdef/recdef.cmo \
+    pretyping/rawterm.cmi proofs/proof_type.cmi parsing/printer.cmi \
+    pretyping/pretyping.cmi parsing/ppconstr.cmi lib/pp.cmi proofs/pfedit.cmi \
+    lib/options.cmi kernel/names.cmi library/libnames.cmi \
+    pretyping/indrec.cmi contrib/funind/indfun_common.cmi \
+    tactics/hiddentac.cmi library/global.cmi interp/genarg.cmi \
+    pretyping/evd.cmi tactics/equality.cmi kernel/environ.cmi \
+    kernel/entries.cmi tactics/eauto.cmi library/declare.cmi \
+    kernel/declarations.cmi library/decl_kinds.cmo interp/coqlib.cmi \
+    toplevel/command.cmi kernel/closure.cmi pretyping/clenv.cmi \
+    toplevel/cerrors.cmi contrib/funind/new_arg_principle.cmi 
 contrib/funind/new_arg_principle.cmx: toplevel/vernacexpr.cmx \
     toplevel/vernacentries.cmx lib/util.cmx pretyping/unification.cmx \
-    pretyping/termops.cmx kernel/term.cmx tactics/tactics.cmx \
-    tactics/tacticals.cmx proofs/tactic_debug.cmx pretyping/tacred.cmx \
-    proofs/tacmach.cmx tactics/tacinterp.cmx pretyping/reductionops.cmx \
-    contrib/recdef/recdef.cmx pretyping/rawterm.cmx proofs/proof_type.cmx \
-    parsing/printer.cmx lib/pp.cmx proofs/pfedit.cmx lib/options.cmx \
-    kernel/names.cmx library/libnames.cmx pretyping/indrec.cmx \
-    contrib/funind/indfun_common.cmx tactics/hiddentac.cmx library/global.cmx \
-    interp/genarg.cmx pretyping/evd.cmx tactics/equality.cmx \
-    kernel/environ.cmx kernel/entries.cmx tactics/eauto.cmx \
-    library/declare.cmx kernel/declarations.cmx library/decl_kinds.cmx \
-    interp/coqlib.cmx toplevel/command.cmx kernel/closure.cmx \
-    pretyping/clenv.cmx toplevel/cerrors.cmx \
-    contrib/funind/new_arg_principle.cmi 
+    pretyping/typing.cmx pretyping/termops.cmx kernel/term.cmx \
+    tactics/tactics.cmx tactics/tacticals.cmx proofs/tactic_debug.cmx \
+    pretyping/tacred.cmx proofs/tacmach.cmx tactics/tacinterp.cmx \
+    pretyping/reductionops.cmx contrib/recdef/recdef.cmx \
+    pretyping/rawterm.cmx proofs/proof_type.cmx parsing/printer.cmx \
+    pretyping/pretyping.cmx parsing/ppconstr.cmx lib/pp.cmx proofs/pfedit.cmx \
+    lib/options.cmx kernel/names.cmx library/libnames.cmx \
+    pretyping/indrec.cmx contrib/funind/indfun_common.cmx \
+    tactics/hiddentac.cmx library/global.cmx interp/genarg.cmx \
+    pretyping/evd.cmx tactics/equality.cmx kernel/environ.cmx \
+    kernel/entries.cmx tactics/eauto.cmx library/declare.cmx \
+    kernel/declarations.cmx library/decl_kinds.cmx interp/coqlib.cmx \
+    toplevel/command.cmx kernel/closure.cmx pretyping/clenv.cmx \
+    toplevel/cerrors.cmx contrib/funind/new_arg_principle.cmi 
 contrib/funind/rawtermops.cmo: lib/util.cmi proofs/tactic_debug.cmi \
     tactics/tacinterp.cmi pretyping/rawterm.cmi parsing/printer.cmi \
     parsing/ppconstr.cmi lib/pp.cmi kernel/names.cmi library/nameops.cmi \
@@ -3735,6 +3741,8 @@ tactics/eauto.cmo: parsing/grammar.cma
 tactics/eauto.cmx: parsing/grammar.cma
 toplevel/whelp.cmo: parsing/grammar.cma
 toplevel/whelp.cmx: parsing/grammar.cma
+tactics/hipattern.cmo: parsing/grammar.cma parsing/q_constr.cmo
+tactics/hipattern.cmx: parsing/grammar.cma parsing/q_constr.cmo
 contrib/omega/g_omega.cmo: parsing/grammar.cma
 contrib/omega/g_omega.cmx: parsing/grammar.cma
 contrib/romega/g_romega.cmo: parsing/grammar.cma
@@ -3807,6 +3815,8 @@ parsing/tacextend.cmo:
 parsing/tacextend.cmx: 
 parsing/vernacextend.cmo: 
 parsing/vernacextend.cmx: 
+parsing/q_constr.cmo: 
+parsing/q_constr.cmx: 
 toplevel/mltop.cmo: 
 toplevel/mltop.cmx: 
 lib/pp.cmo: 
@@ -3826,58 +3836,58 @@ tools/coq_makefile.cmx:
 tools/coq-tex.cmo: 
 tools/coq-tex.cmx: 
 coq_fix_code.o: kernel/byterun/coq_fix_code.c \
-  /usr/lib/ocaml/3.09.1/caml/config.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
 coq_interp.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
-  /usr/lib/ocaml/3.09.1/caml/alloc.h kernel/byterun/coq_instruct.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
   kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
-  /usr/lib/ocaml/3.09.1/caml/alloc.h kernel/byterun/coq_instruct.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h
 coq_values.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \
-  kernel/byterun/coq_values.h /usr/lib/ocaml/3.09.1/caml/alloc.h
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h
 coq_fix_code.d.o: kernel/byterun/coq_fix_code.c \
-  /usr/lib/ocaml/3.09.1/caml/config.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/misc.h /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \
+  /usr/local/lib/ocaml/caml/config.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/misc.h /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_fix_code.h
 coq_interp.d.o: kernel/byterun/coq_interp.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
-  /usr/lib/ocaml/3.09.1/caml/alloc.h kernel/byterun/coq_instruct.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
   kernel/byterun/coq_values.h kernel/byterun/coq_jumptbl.h
 coq_memory.d.o: kernel/byterun/coq_memory.c kernel/byterun/coq_gc.h \
-  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
-  /usr/lib/ocaml/3.09.1/caml/alloc.h kernel/byterun/coq_instruct.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
+  /usr/local/lib/ocaml/caml/alloc.h kernel/byterun/coq_instruct.h \
   kernel/byterun/coq_fix_code.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h
 coq_values.d.o: kernel/byterun/coq_values.c kernel/byterun/coq_fix_code.h \
-  /usr/lib/ocaml/3.09.1/caml/mlvalues.h \
-  /usr/lib/ocaml/3.09.1/caml/compatibility.h \
-  /usr/lib/ocaml/3.09.1/caml/config.h /usr/lib/ocaml/3.09.1/caml/misc.h \
+  /usr/local/lib/ocaml/caml/mlvalues.h \
+  /usr/local/lib/ocaml/caml/compatibility.h \
+  /usr/local/lib/ocaml/caml/config.h /usr/local/lib/ocaml/caml/misc.h \
   kernel/byterun/coq_instruct.h kernel/byterun/coq_memory.h \
-  /usr/lib/ocaml/3.09.1/caml/fail.h /usr/lib/ocaml/3.09.1/caml/memory.h \
-  kernel/byterun/coq_values.h /usr/lib/ocaml/3.09.1/caml/alloc.h
+  /usr/local/lib/ocaml/caml/fail.h /usr/local/lib/ocaml/caml/memory.h \
+  kernel/byterun/coq_values.h /usr/local/lib/ocaml/caml/alloc.h
diff --git a/.depend.camlp4 b/.depend.camlp4
index 741158e9b..ba5ebda57 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -4,6 +4,7 @@ tactics/extraargs.ml: parsing/grammar.cma
 tactics/extratactics.ml: parsing/grammar.cma
 tactics/eauto.ml: parsing/grammar.cma
 toplevel/whelp.ml: parsing/grammar.cma
+tactics/hipattern.ml: parsing/grammar.cma parsing/q_constr.cmo
 contrib/omega/g_omega.ml: parsing/grammar.cma
 contrib/romega/g_romega.ml: parsing/grammar.cma
 contrib/ring/g_quote.ml: parsing/grammar.cma
@@ -40,6 +41,7 @@ parsing/g_ltac.ml:
 parsing/argextend.ml: 
 parsing/tacextend.ml: 
 parsing/vernacextend.ml: 
+parsing/q_constr.ml: 
 toplevel/mltop.ml: 
 lib/pp.ml: 
 lib/compat.ml: 
diff --git a/Makefile b/Makefile
index c3aa91915..aca30acba 100644
--- a/Makefile
+++ b/Makefile
@@ -208,7 +208,7 @@ HIGHTACTICS=\
 SPECTAC= tactics/tauto.ml4 tactics/eqdecide.ml4
 USERTAC = $(SPECTAC)
 ML4FILES += $(USERTAC) tactics/extraargs.ml4 tactics/extratactics.ml4 \
-	tactics/eauto.ml4 toplevel/whelp.ml4
+	tactics/eauto.ml4 toplevel/whelp.ml4 tactics/hipattern.ml4
 
 USERTACCMO=$(USERTAC:.ml4=.cmo)
 USERTACCMX=$(USERTAC:.ml4=.cmx)
@@ -1413,7 +1413,7 @@ ML4FILES +=parsing/g_minicoq.ml4 \
 	   parsing/g_xml.ml4 parsing/g_constr.ml4 \
 	   parsing/g_tactic.ml4 parsing/g_ltac.ml4 \
 	   parsing/argextend.ml4 parsing/tacextend.ml4 \
-	   parsing/vernacextend.ml4
+	   parsing/vernacextend.ml4 parsing/q_constr.ml4
 
 # beforedepend:: $(GRAMMARCMO)
 
diff --git a/parsing/q_constr.ml4 b/parsing/q_constr.ml4
new file mode 100644
index 000000000..768bc45c1
--- /dev/null
+++ b/parsing/q_constr.ml4
@@ -0,0 +1,124 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+(* $Id: g_constr.ml4,v 1.58 2005/12/30 10:55:32 herbelin Exp $ *)
+
+open Rawterm
+open Term
+open Names
+open Pattern
+open Q_util
+open Util
+open Pcaml
+
+let loc = dummy_loc
+let dloc = <:expr< Util.dummy_loc >>
+
+let apply_ref f l = 
+  <:expr< 
+    Rawterm.RApp ($dloc$, Rawterm.RRef ($dloc$, Lazy.force $f$), $mlexpr_of_list (fun x -> x) l$)
+  >>
+
+EXTEND
+  GLOBAL: expr;
+  expr:
+    [ [ "PATTERN"; "["; c = constr; "]" ->
+      <:expr< snd (Pattern.pattern_of_rawconstr $c$) >> ] ]
+  ;
+  sort:
+    [ [ "Set"  -> RProp Pos
+      | "Prop" -> RProp Null
+      | "Type" -> RType None ] ]
+  ;
+  ident:
+    [ [ s = string -> <:expr< Names.id_of_string $str:s$ >> ] ]
+  ;
+  name:
+    [ [ "_" -> <:expr< Anonymous >> | id = ident -> <:expr< Name $id$ >> ] ]
+  ;
+  string:
+    [ [ UIDENT | LIDENT ] ]
+  ;
+  constr:
+    [ "200" RIGHTA
+      [ LIDENT "forall"; id = ident; ":"; c1 = constr; ","; c2 = constr ->
+        <:expr< Rawterm.RProd ($dloc$,Name $id$,$c1$,$c2$) >>
+      | "fun"; id = ident; ":"; c1 = constr; "=>"; c2 = constr ->
+        <:expr< Rawterm.RLambda ($dloc$,Name $id$,$c1$,$c2$) >>
+      | "let"; id = ident; ":="; c1 = constr; "in"; c2 = constr ->
+        <:expr< Rawterm.RLetin ($dloc$,Name $id$,$c1$,$c2$) >>
+      (* fix todo *)
+      ]
+    | "100" RIGHTA
+      [ c1 = constr; ":"; c2 = SELF -> 
+        <:expr< Rawterm.RCast($dloc$,$c1$,DEFAULTcast,$c2$) >> ]
+    | "90" RIGHTA
+      [ c1 = constr; "->"; c2 = SELF -> 
+        <:expr< Rawterm.RProd ($dloc$,Anonymous,$c1$,$c2$) >> ]
+    | "75" RIGHTA
+      [ "~"; c = constr -> 
+        apply_ref <:expr< coq_not_ref >> [c] ]
+    | "70" RIGHTA
+      [ c1 = constr; "="; c2 = NEXT; ":>"; t = NEXT ->
+        apply_ref <:expr< coq_eq_ref >> [t;c1;c2] ]
+    | "10" LEFTA
+      [ f = constr; args = LIST1 NEXT ->
+        let args = mlexpr_of_list (fun x -> x) args in
+        <:expr< Rawterm.RApp ($dloc$,$f$,$args$) >> ]
+    | "0"
+      [ s = sort -> <:expr< Rawterm.RSort ($dloc$,s) >>
+      | id = ident -> <:expr< Rawterm.RVar ($dloc$,$id$) >>
+      | "_" -> <:expr< Rawterm.RHole ($dloc$,QuestionMark) >>
+      | "?"; id = ident -> <:expr< Rawterm.RPatVar($dloc$,(False,$id$)) >>
+      | "{"; c1 = constr; "}"; "+"; "{"; c2 = constr; "}" ->
+          apply_ref <:expr< coq_sumbool_ref >> [c1;c2]
+      | "%"; e = string -> <:expr< Rawterm.RRef ($dloc$,Lazy.force $lid:e$) >>
+      | c = match_constr -> c
+      | "("; c = constr LEVEL "200"; ")" -> c ] ]
+  ;
+  match_constr:
+    [ [ "match"; c = constr LEVEL "100"; (ty,nal) = match_type;
+        "with"; OPT"|"; br = LIST0 eqn SEP "|"; "end" -> 
+          let br = mlexpr_of_list (fun x -> x) br in
+     <:expr< Rawterm.RCases ($dloc$,$ty$,[($c$,$nal$)],$br$) >> 
+    ] ]
+  ;
+  match_type:
+    [ [ "as"; id = ident; "in"; ind = LIDENT; nal = LIST0 name;  
+        "return"; ty = constr LEVEL "100" -> 
+          let nal = mlexpr_of_list (fun x -> x) nal in
+          <:expr< Some $ty$ >>, 
+          <:expr< (Name $id$, Some ($dloc$,$lid:ind$,$nal$)) >> 
+      | -> <:expr< None >>, <:expr< (Anonymous, None) >> ] ]
+  ;
+  eqn:
+    [ [ (lid,pl) = pattern; "=>"; rhs = constr -> 
+        let lid = mlexpr_of_list (fun x -> x) lid in
+        <:expr< ($dloc$,$lid$,[$pl$],$rhs$) >> 
+    ] ]
+  ;
+  pattern: 
+    [ [ "%"; e = string; lip = LIST0 patvar ->
+        let lp = mlexpr_of_list (fun (_,x) -> x) lip in
+        let lid = List.flatten (List.map fst lip) in
+        lid, <:expr< Rawterm.PatCstr ($dloc$,$lid:e$,$lp$,Anonymous) >>
+      | p = patvar -> p
+      | "("; p = pattern; ")" -> p ] ]
+  ;
+  patvar:
+    [ [ "_" -> [], <:expr< Rawterm.PatVar ($dloc$,Anonymous) >> 
+      | id = ident -> [id], <:expr< Rawterm.PatVar ($dloc$,Name $id$) >> 
+    ] ]
+  ;
+  END;;
+
+(* Example 
+open Coqlib
+let a = PATTERN [ match ?X with %path_of_S n => n | %path_of_O => ?X end ]
+*)
+
diff --git a/tactics/eqdecide.ml4 b/tactics/eqdecide.ml4
index 4bd83c672..8a1c4e16a 100644
--- a/tactics/eqdecide.ml4
+++ b/tactics/eqdecide.ml4
@@ -46,11 +46,11 @@ open Coqlib
    2. Try discrimination to solve those goals where x and y has
       been introduced by different constructors.
    3. If x and y have been introduced by the same constructor,
-      then analyse one by one the correspoing pairs of arguments.
+      then analyse one by one the corresponding pairs of arguments.
       If they are equal, rewrite one into the other. If they are
       not, derive a contradiction from the injectiveness of the
       constructor. 
-   4. Once all the arguments have been rewritten, solve the left half 
+   4. Once all the arguments have been rewritten, solve the remaining half 
       of the disjunction by reflexivity.
 
    Eduardo Gimenez (30/3/98).
@@ -58,35 +58,36 @@ open Coqlib
 
 let clear_last = (tclLAST_HYP (fun c -> (clear [destVar c])))
 
-let mkBranches = 
+let choose_eq eqonleft = 
+  if eqonleft then h_simplest_left else h_simplest_right
+let choose_noteq eqonleft =
+  if eqonleft then h_simplest_right else h_simplest_left
+
+let mkBranches c1 c2 = 
   tclTHENSEQ
-    [intro; 
-     tclLAST_HYP h_simplest_elim;
-     clear_last;
-     intros ;
+    [generalize [c2];
+     h_simplest_elim c1;
+     intros;
      tclLAST_HYP h_simplest_case;
      clear_last;
      intros]
 
-let solveRightBranch  = 
-  tclTHEN h_simplest_right
+let solveNoteqBranch side = 
+  tclTHEN (choose_noteq side)
     (tclTHEN (intro_force true)
       (onLastHyp (fun id -> Extratactics.h_discrHyp (Rawterm.NamedHyp id))))
 
-let h_solveRightBranch =
-  Refiner.abstract_extended_tactic "solveRightBranch" [] solveRightBranch
-
-(*
-let h_solveRightBranch =
-  hide_atomic_tactic "solveRightBranch" solveRightBranch
-*)
+let h_solveNoteqBranch side =
+  Refiner.abstract_extended_tactic "solveNoteqBranch" [] 
+    (solveNoteqBranch side)
 
 (* Constructs the type {c1=c2}+{~c1=c2} *)
 
-let mkDecideEqGoal rectype c1 c2 g = 
+let mkDecideEqGoal eqonleft op rectype c1 c2 g = 
   let equality    = mkApp(build_coq_eq(), [|rectype; c1; c2|]) in
   let disequality = mkApp(build_coq_not (), [|equality|]) in
-  mkApp(build_coq_sumbool (), [|equality; disequality |])
+  if eqonleft then mkApp(op, [|equality; disequality |])
+  else mkApp(op, [|disequality; equality |])
 
 
 (* Constructs the type (x1,x2:R){x1=x2}+{~x1=x2} *)
@@ -97,42 +98,45 @@ let mkGenDecideEqGoal rectype g =
   and yname    = next_ident_away (id_of_string "y") hypnames in
   (mkNamedProd xname rectype 
      (mkNamedProd yname rectype 
-        (mkDecideEqGoal rectype (mkVar xname) (mkVar yname) g)))
+        (mkDecideEqGoal true (build_coq_sumbool ())
+          rectype (mkVar xname) (mkVar yname) g)))
 
-let eqCase  tac = 
+let eqCase tac = 
   (tclTHEN intro  
   (tclTHEN (tclLAST_HYP Extratactics.h_rewriteLR)
   (tclTHEN clear_last 
   tac)))
 
-let diseqCase = 
+let diseqCase eqonleft =
   let diseq  = id_of_string "diseq" in
   let absurd = id_of_string "absurd" in 
   (tclTHEN (intro_using diseq)
-  (tclTHEN  h_simplest_right
+  (tclTHEN (choose_noteq eqonleft)
   (tclTHEN  red_in_concl
   (tclTHEN  (intro_using absurd)
   (tclTHEN  (h_simplest_apply (mkVar diseq))
   (tclTHEN  (Extratactics.h_injHyp (Rawterm.NamedHyp absurd))
             (full_trivial [])))))))
 
-let solveArg a1 a2 tac  g = 
+let solveArg eqonleft op a1 a2 tac g = 
   let rectype = pf_type_of g a1 in
-  let decide  = mkDecideEqGoal rectype a1 a2 g in  
-  (tclTHENS
-     (h_elim_type decide) 
-     [(eqCase tac);diseqCase;default_auto]) g
+  let decide  = mkDecideEqGoal eqonleft op rectype a1 a2 g in
+  let subtacs = 
+    if eqonleft then [eqCase tac;diseqCase eqonleft;default_auto] 
+    else [diseqCase eqonleft;eqCase tac;default_auto] in
+  (tclTHENS (h_elim_type decide) subtacs) g
 
-let solveLeftBranch rectype g =
+let solveEqBranch rectype g =
   try
-    let (lhs,rhs) = match_eqdec_partial (pf_concl g) in
+    let (eqonleft,op,lhs,rhs,_) = match_eqdec (pf_concl g) in
     let (mib,mip) = Global.lookup_inductive rectype in
     let nparams   = mib.mind_nparams in
     let getargs l = list_skipn nparams (snd (decompose_app l)) in
     let rargs   = getargs rhs
     and largs   = getargs lhs in 
     List.fold_right2 
-      solveArg largs rargs (tclTHEN h_simplest_left h_reflexivity) g
+      (solveArg eqonleft op) largs rargs
+      (tclTHEN (choose_eq eqonleft) h_reflexivity) g
   with PatternMatchingFailure -> error "Unexpected conclusion!"
 
 (* The tactic Decide Equality *)
@@ -143,31 +147,33 @@ let hd_app c = match kind_of_term c with
 
 let decideGralEquality g =
   try
-    let typ = match_eqdec (pf_concl g) in
+    let eqonleft,_,c1,c2,typ = match_eqdec (pf_concl g) in
     let headtyp = hd_app (pf_compute g typ) in
     let rectype =
       match kind_of_term headtyp with
         | Ind mi -> mi
 	| _ -> error "This decision procedure only works for inductive objects"
-    in 
+    in
     (tclTHEN
-      mkBranches 
-      (tclORELSE h_solveRightBranch (solveLeftBranch rectype))) g
+      (mkBranches c1 c2)
+      (tclORELSE (h_solveNoteqBranch eqonleft) (solveEqBranch rectype)))
+    g
   with PatternMatchingFailure ->
-    error "The goal does not have the expected form"
+    error "The goal must be of the form {x<>y}+{x=y} or {x=y}+{x<>y}"
 
+let decideEqualityGoal = tclTHEN intros decideGralEquality
 
 let decideEquality c1 c2 g = 
   let rectype = (pf_type_of g c1) in     
   let decide  = mkGenDecideEqGoal rectype g in  
-  (tclTHENS (cut decide) [default_auto;decideGralEquality]) g
+  (tclTHENS (cut decide) [default_auto;decideEqualityGoal]) g
 
 
 (* The tactic Compare *)
 
 let compare c1 c2 g = 
   let rectype = pf_type_of g c1 in
-  let decide  = mkDecideEqGoal rectype c1 c2 g in  
+  let decide  = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 g in  
   (tclTHENS (cut decide) 
             [(tclTHEN  intro 
              (tclTHEN (tclLAST_HYP simplest_case)
@@ -179,10 +185,9 @@ let compare c1 c2 g =
 
 TACTIC EXTEND decide_equality
   [ "decide" "equality" constr(c1) constr(c2) ] -> [ decideEquality c1 c2 ]
-| [ "decide" "equality" ] -> [ decideGralEquality ]
+| [ "decide" "equality" ] -> [ decideEqualityGoal ]
 END
 
 TACTIC EXTEND compare
 | [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
 END
-
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml4
index fd2d5c9c1..e35623b52 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml4
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i camlp4deps: "parsing/grammar.cma parsing/q_constr.cmo" i*)
+
 (* $Id$ *)
 
 open Pp
@@ -40,7 +42,6 @@ type 'a matching_function = constr -> 'a option
 type testing_function  = constr -> bool
 
 let mkmeta n = Nameops.make_ident "X" (Some n)
-let mkPMeta n = PMeta (Some (mkmeta n))
 let meta1 = mkmeta 1
 let meta2 = mkmeta 2
 let meta3 = mkmeta 3
@@ -133,21 +134,9 @@ let is_unit_type t = op2bool (match_with_unit_type t)
    inductive binary relation R, so that R has only one constructor
    establishing its reflexivity.  *)
 
-(* ["(A : ?)(x:A)(? A x x)"] and ["(x : ?)(? x x)"] *)
-let x = Name (id_of_string "x")
-let y = Name (id_of_string "y")
-let name_A = Name (id_of_string "A")
-let coq_refl_rel1_pattern =
-  PProd
-    (name_A, PMeta None,
-    PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 1|])))
-let coq_refl_rel2_pattern =
-  PProd (x, PMeta None, PApp (PMeta None, [|PRel 1; PRel 1|]))
-
-let coq_refl_reljm_pattern =
-PProd
-    (name_A, PMeta None,
-    PProd (x, PRel 1, PApp (PMeta None, [|PRel 2; PRel 1; PRel 2;PRel 1|])))
+let coq_refl_rel1_pattern  = PATTERN [ forall A:_, forall x:A, _ A x x ]
+let coq_refl_rel2_pattern  = PATTERN [ forall x:_, _ x x ]
+let coq_refl_reljm_pattern = PATTERN [ forall A:_, forall x:A, _ A x A x ]
 
 let match_with_equation t =
   let (hdapp,args) = decompose_app t in
@@ -168,9 +157,8 @@ let match_with_equation t =
 
 let is_equation t = op2bool (match_with_equation  t)
 
-(* ["(?1 -> ?2)"] *)
-let imp a b = PProd (Anonymous, a, b)
-let coq_arrow_pattern = imp (mkPMeta 1) (mkPMeta 2)
+let coq_arrow_pattern = PATTERN [ ?X1 -> ?X2 ]
+
 let match_arrow_pattern t =
   match matches coq_arrow_pattern t with
     | [(m1,arg);(m2,mind)] -> assert (m1=meta1 & m2=meta2); (arg, mind)
@@ -253,10 +241,8 @@ let rec first_match matcher = function
 (*** Equality *)
 
 (* Patterns "(eq ?1 ?2 ?3)" and "(identity ?1 ?2 ?3)" *)
-let coq_eq_pattern_gen eq = 
-  lazy (PApp(PRef (Lazy.force eq), [|mkPMeta 1;mkPMeta 2;mkPMeta 3|]))
+let coq_eq_pattern_gen eq = lazy PATTERN [ %eq ?X1 ?X2 ?X3 ]
 let coq_eq_pattern = coq_eq_pattern_gen coq_eq_ref
-(*let coq_eqT_pattern = coq_eq_pattern_gen coq_eqT_ref*)
 let coq_identity_pattern = coq_eq_pattern_gen coq_identity_ref
 
 let match_eq eqn eq_pat =
@@ -292,8 +278,7 @@ let dest_nf_eq gls eqn =
 (*** Sigma-types *)
 
 (* Patterns "(existS ?1 ?2 ?3 ?4)" and "(existT ?1 ?2 ?3 ?4)" *)
-let coq_ex_pattern_gen ex =
-  lazy(PApp(PRef (Lazy.force ex), [|mkPMeta 1;mkPMeta 2;mkPMeta 3;mkPMeta 4|]))
+let coq_ex_pattern_gen ex = lazy PATTERN [ %ex ?X1 ?X2 ?X3 ?X4 ]
 let coq_existS_pattern = coq_ex_pattern_gen coq_existS_ref
 let coq_existT_pattern = coq_ex_pattern_gen coq_existT_ref
 
@@ -311,8 +296,7 @@ let find_sigma_data_decompose ex = (* fails with PatternMatchingFailure *)
      coq_existT_pattern, build_sigma_type]
 
 (* Pattern "(sig ?1 ?2)" *)
-let coq_sig_pattern = 
-  lazy (PApp (PRef (Lazy.force coq_sig_ref), [| (mkPMeta 1); (mkPMeta 2) |]))
+let coq_sig_pattern = lazy PATTERN [ %coq_sig_ref ?X1 ?X2 ]
 
 let match_sigma t =
   match matches (Lazy.force coq_sig_pattern) t with
@@ -323,43 +307,47 @@ let is_matching_sigma t = is_matching (Lazy.force coq_sig_pattern) t
 
 (*** Decidable equalities *)
 
-(* Pattern "(sumbool (eq ?1 ?2 ?3) ?4)" *)
-let coq_eqdec_partial_pattern =
-  lazy
-    (PApp
-       (PRef (Lazy.force coq_sumbool_ref),
-	[| Lazy.force coq_eq_pattern; (mkPMeta 4) |]))
+(* The expected form of the goal for the tactic Decide Equality *)
 
-let match_eqdec_partial t =
-  match matches (Lazy.force coq_eqdec_partial_pattern) t with
-    | [_; (_,lhs); (_,rhs); _] -> (lhs,rhs)
-    | _ -> anomaly "Unexpected pattern"
+(* Pattern "{<?1>x=y}+{~(<?1>x=y)}" *)
+(* i.e. "(sumbool (eq ?1 x y) ~(eq ?1 x y))" *)
 
-(* The expected form of the goal for the tactic Decide Equality *)
+let coq_eqdec_inf_pattern =
+ lazy PATTERN [ { ?X2 = ?X3 :> ?X1 } + { ~ ?X2 = ?X3 :> ?X1 } ]
+
+let coq_eqdec_inf_rev_pattern =
+ lazy PATTERN [ { ~ ?X2 = ?X3 :> ?X1 } + { ?X2 = ?X3 :> ?X1 } ]
 
-(* Pattern "(x,y:?1){<?1>x=y}+{~(<?1>x=y)}" *)
-(* i.e. "(x,y:?1)(sumbool (eq ?1 x y) ~(eq ?1 x y))" *)
-let x = Name (id_of_string "x")
-let y = Name (id_of_string "y")
 let coq_eqdec_pattern =
-  lazy
-    (PProd (x, (mkPMeta 1), PProd (y, (mkPMeta 1), 
-    PApp (PRef (Lazy.force coq_sumbool_ref),
-	  [| PApp (PRef (Lazy.force coq_eq_ref),
-		   [| (mkPMeta 1); PRel 2; PRel 1 |]);
-	     PApp (PRef (Lazy.force coq_not_ref), 
-		   [|PApp (PRef (Lazy.force coq_eq_ref),
- 			   [| (mkPMeta 1); PRel 2; PRel 1 |])|]) |]))))
+ lazy PATTERN [ %coq_or_ref (?X2 = ?X3 :> ?X1) (~ ?X2 = ?X3 :> ?X1) ]
+
+let coq_eqdec_rev_pattern =
+ lazy PATTERN [ %coq_or_ref (~ ?X2 = ?X3 :> ?X1) (?X2 = ?X3 :> ?X1) ]
+
+let op_or = coq_or_ref
+let op_sum = coq_sumbool_ref
 
 let match_eqdec t =
-  match matches (Lazy.force coq_eqdec_pattern) t with
-    | [(_,typ)] -> typ
-    | _ -> anomaly "Unexpected pattern"
+  let eqonleft,op,subst =
+    try true,op_sum,matches (Lazy.force coq_eqdec_inf_pattern) t
+    with PatternMatchingFailure -> 
+    try false,op_sum,matches (Lazy.force coq_eqdec_inf_rev_pattern) t
+    with PatternMatchingFailure -> 
+    try true,op_or,matches (Lazy.force coq_eqdec_pattern) t
+    with PatternMatchingFailure -> 
+        false,op_or,matches (Lazy.force coq_eqdec_rev_pattern) t in
+  match subst with
+  | [(_,typ);(_,c1);(_,c2)] -> 
+      eqonleft, Libnames.constr_of_global (Lazy.force op), c1, c2, typ
+  | _ -> anomaly "Unexpected pattern"
 
 (* Patterns "~ ?" and "? -> False" *)
-let coq_not_pattern = lazy(PApp(PRef (Lazy.force coq_not_ref), [|PMeta None|]))
-let coq_imp_False_pattern =
-  lazy (imp (PMeta None) (PRef (Lazy.force coq_False_ref)))
+let coq_not_pattern = lazy PATTERN [ ~ _ ]
+let coq_imp_False_pattern = lazy PATTERN [ _ -> %coq_False_ref ]
 
 let is_matching_not t = is_matching (Lazy.force coq_not_pattern) t
 let is_matching_imp_False t = is_matching (Lazy.force coq_imp_False_pattern) t
+
+(* Remark: patterns that have references to the standard library must
+   be evaluated lazily (i.e. at the time they are used, not a the time
+   coqtop starts) *)
diff --git a/tactics/hipattern.mli b/tactics/hipattern.mli
index 04d4566cb..67040c15d 100644
--- a/tactics/hipattern.mli
+++ b/tactics/hipattern.mli
@@ -96,7 +96,7 @@ val is_sigma_type           : testing_function
 
 open Coqlib
 
-(* Match terms [(eq A t u)], [(eqT A t u)] or [(identityT A t u)] *)
+(* Match terms [(eq A t u)] or [(identity A t u)] *)
 (* Returns associated lemmas and [A,t,u] *)
 val find_eq_data_decompose : constr -> 
   coq_leibniz_eq_data * (constr * constr * constr)
@@ -111,11 +111,9 @@ val match_sigma : constr -> constr * constr
 
 val is_matching_sigma : constr -> bool
 
-(* Match a term of the form [{x=y}+{_}], returns [x] and [y] *)
-val match_eqdec_partial : constr -> constr * constr
-
-(* Match a term of the form [(x,y:t){x=y}+{~x=y}], returns [t] *)
-val match_eqdec : constr -> constr
+(* Match a decidable equality judgement (e.g [{t=u:>T}+{~t=u}]), returns
+   [t,u,T] and a boolean telling if equality is on the left side *)
+val match_eqdec : constr -> bool * constr * constr * constr * constr
 
 (* Match an equality up to conversion; returns [(eq,t1,t2)] in normal form *)
 open Proof_type