diff options
| -rw-r--r-- | .depend | 16 | ||||
| -rw-r--r-- | parsing/search.ml | 11 |
2 files changed, 15 insertions, 12 deletions
@@ -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) | _ -> ()) | _ -> () |