diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 22:12:16 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 22:12:16 +0000 |
| commit | 2f5c0f8880cd4ccc27cef4980768d35c9ebd26ea (patch) | |
| tree | fb1f33855c930c0f5c46a67529e6df6e24652c9f /interp | |
| parent | 30ef31fd8e01d39fb7ce909167dcc1e4a29d7f80 (diff) | |
Types inductifs parametriques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 2 | ||||
| -rw-r--r-- | interp/constrintern.ml | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index a5b022058..8faec21df 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1254,7 +1254,7 @@ let rec match_cases_pattern metas sigma a1 a2 = match (a1,a2) with | a, AHole _ when not(Options.do_translate()) -> sigma | PatCstr (loc,(ind,_ as r1),args1,Anonymous), _ -> let nparams = - (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in + (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let l2 = match a2 with | ARef (ConstructRef r2) when r1 = r2 -> [] diff --git a/interp/constrintern.ml b/interp/constrintern.ml index b2b657c5f..498c483dc 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -462,7 +462,7 @@ let subst_cases_pattern loc (ids,asubst as aliases) intern subst scopes a = | ARef (ConstructRef c) -> (ids,[asubst, PatCstr (loc,c, [], alias_of aliases)]) | AApp (ARef (ConstructRef (ind,_ as c)),args) -> - let nparams = (snd (Global.lookup_inductive ind)).Declarations.mind_nparams in + let nparams = (fst (Global.lookup_inductive ind)).Declarations.mind_nparams in let _,args = list_chop nparams args in let idslpll = List.map (aux ([],[]) subst) args in let ids',pll = product_of_cases_patterns ids idslpll in @@ -500,7 +500,7 @@ let rec patt_of_rawterm loc cstr = | RApp (_,RApp(_,h,l1),l2) -> patt_of_rawterm loc (RApp(loc,h,l1@l2)) | RApp (_,RRef(_,(ConstructRef c as x)),pl) -> if !dump then add_glob loc x; - let (_,mib) = Inductive.lookup_mind_specif (Global.env()) (fst c) in + let (mib,_) = Inductive.lookup_mind_specif (Global.env()) (fst c) in let npar = mib.Declarations.mind_nparams in let (params,args) = if List.length pl <= npar then (pl,[]) else |