diff options
| author |  bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-10 13:50:34 +0000 |
|---|---|---|
| committer | bertot <bertot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-04-10 13:50:34 +0000 |
| commit | 45d82e91c30f912740211060b4cdb7cb83226157 (patch) | |
| tree | 69aeeff425a9edaefb7139497d33720b91f13cc4 /parsing | |
| parent | 2bb2d480b547e58deb2ec62791c8990ecac777b0 (diff) | |
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
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/search.ml | 11 |
1 files changed, 7 insertions, 4 deletions
diff --git a/parsing/search.ml b/parsing/search.ml index 88ab104ef..a4053757f 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) | _ -> ()) | _ -> () |