Modified searchPattern. Before this correction, constructors were overlooked,

because the observation was done on the internal data-structure provided in
the inductive definition.  But this internal data-structure is not well-suited
pattern-matching, since it contains debruijn indices where the inductive type
should occur.


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

2 files changed, 15 insertions, 12 deletions

diff --git a/.depend b/.depend
index 1bc5ebc1b8..8b7bc1691e 100644
--- a/.depend
+++ b/.depend
@@ -612,13 +612,15 @@ parsing/search.cmo: parsing/astterm.cmi parsing/coqast.cmi \
     kernel/declarations.cmi library/declare.cmi kernel/environ.cmi \
     kernel/evd.cmi library/global.cmi library/libobject.cmi \
     library/library.cmi kernel/names.cmi pretyping/pattern.cmi lib/pp.cmi \
-    parsing/pretty.cmi parsing/printer.cmi kernel/term.cmi \
+    parsing/pretty.cmi pretyping/pretyping.cmi parsing/printer.cmi \
+    pretyping/rawterm.cmi pretyping/retyping.cmi kernel/term.cmi \
     pretyping/typing.cmi lib/util.cmi parsing/search.cmi 
 parsing/search.cmx: parsing/astterm.cmx parsing/coqast.cmx \
     kernel/declarations.cmx library/declare.cmx kernel/environ.cmx \
     kernel/evd.cmx library/global.cmx library/libobject.cmx \
     library/library.cmx kernel/names.cmx pretyping/pattern.cmx lib/pp.cmx \
-    parsing/pretty.cmx parsing/printer.cmx kernel/term.cmx \
+    parsing/pretty.cmx pretyping/pretyping.cmx parsing/printer.cmx \
+    pretyping/rawterm.cmx pretyping/retyping.cmx kernel/term.cmx \
     pretyping/typing.cmx lib/util.cmx parsing/search.cmi 
 parsing/termast.cmo: parsing/ast.cmi pretyping/classops.cmi \
     parsing/coqast.cmi library/declare.cmi pretyping/detyping.cmi \
@@ -1292,13 +1294,11 @@ toplevel/toplevel.cmx: parsing/ast.cmx toplevel/errors.cmx library/lib.cmx \
     toplevel/vernac.cmx toplevel/vernacinterp.cmx toplevel/toplevel.cmi 
 toplevel/usage.cmo: config/coq_config.cmi toplevel/usage.cmi 
 toplevel/usage.cmx: config/coq_config.cmx toplevel/usage.cmi 
-toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    toplevel/discharge.cmi library/library.cmi lib/options.cmi \
-    parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi library/states.cmi \
+toplevel/vernac.cmo: parsing/ast.cmi parsing/coqast.cmi library/library.cmi \
+    lib/options.cmi parsing/pcoq.cmi lib/pp.cmi library/states.cmi \
     lib/system.cmi lib/util.cmi toplevel/vernacinterp.cmi toplevel/vernac.cmi 
-toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    toplevel/discharge.cmx library/library.cmx lib/options.cmx \
-    parsing/pcoq.cmx proofs/pfedit.cmx lib/pp.cmx library/states.cmx \
+toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
+    lib/options.cmx parsing/pcoq.cmx lib/pp.cmx library/states.cmx \
     lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
     toplevel/class.cmi pretyping/classops.cmi toplevel/command.cmi \
diff --git a/parsing/search.ml b/parsing/search.ml
index 88ab104ef1..a4053757ff 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -12,6 +12,7 @@ open Pp
 open Util
 open Names
 open Term
+open Rawterm
 open Declarations
 open Libobject
 open Declare
@@ -29,10 +30,13 @@ open Printer
    of the object, the assumptions that will make it possible to print its type,
    and the constr term that represent its type. *)
 
-let print_constructors indsp fn env_ar mip =
+let print_constructors indsp fn env mip =
   let lc = mind_user_lc mip in
   for i=1 to Array.length lc do
-      fn (ConstructRef (indsp,i)) env_ar (lc.(i-1))
+      fn (ConstructRef (indsp,i)) env
+	(Retyping.get_type_of env Evd.empty
+	   (Pretyping.understand Evd.empty env
+	      (RRef(dummy_loc, ConstructRef(indsp,i)))))
   done
 
 let rec head_const c = match kind_of_term c with
@@ -64,11 +68,10 @@ let crible (fn : global_reference -> env -> constr -> unit) ref =
 	      (fun mip ->
 		 (Name mip.mind_typename, None, mip.mind_nf_arity))
 	      mib.mind_packets in
-	  let env_ar = push_rels arities env in
           (match kind_of_term const with 
 	     | IsMutInd ((sp',tyi) as indsp,_) -> 
 		 if sp=sp' then
-		   print_constructors indsp fn env_ar
+		   print_constructors indsp fn env
 		     (mind_nth_type_packet mib tyi)
 	     | _ -> ())
       | _ -> ()