diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-01 02:36:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-01 20:19:53 +0200 |
| commit | 7babf0d42af11f5830bc157a671bd81b478a4f02 (patch) | |
| tree | 428ee1f95355ee5e11c19e12d538e37cc5a81f6c /pretyping/inductiveops.ml | |
| parent | 3df2431a80f9817ce051334cb9c3b1f465bffb60 (diff) | |
Using delayed universe instances in EConstr.
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 88c492f03..5b42add28 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -74,6 +74,7 @@ let substnl_ind_type l n = map_inductive_type (EConstr.Vars.substnl l n) let mkAppliedInd (IndType ((ind,params), realargs)) = let open EConstr in + let ind = on_snd EInstance.make ind in applist (mkIndU ind, (List.map EConstr.of_constr params)@realargs) (* Does not consider imbricated or mutually recursive types *) @@ -471,11 +472,12 @@ let find_rectype env sigma c = let open EConstr in let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with - | Ind (ind,u as indu) -> + | Ind (ind,u) -> let (mib,mip) = Inductive.lookup_mind_specif env ind in if mib.mind_nparams > List.length l then raise Not_found; let l = List.map EConstr.Unsafe.to_constr l in let (par,rargs) = List.chop mib.mind_nparams l in + let indu = (ind, EInstance.kind sigma u) in IndType((indu, par),List.map EConstr.of_constr rargs) | _ -> raise Not_found |