diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-21 12:13:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:34 +0100 |
| commit | 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd (patch) | |
| tree | 101bd3bc2e05eb52bfc142587d425f8920671b25 /pretyping/inductiveops.ml | |
| parent | e09f3b44bb381854b647a6d9debdeddbfc49177e (diff) | |
Reductionops now return EConstrs.
Diffstat (limited to 'pretyping/inductiveops.ml')
| -rw-r--r-- | pretyping/inductiveops.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml index 9c5a2e894..120adb9fe 100644 --- a/pretyping/inductiveops.ml +++ b/pretyping/inductiveops.ml @@ -456,7 +456,7 @@ let extract_mrectype sigma t = let find_mrectype_vect env sigma c = let open EConstr in - let (t, l) = Termops.decompose_app_vect sigma (EConstr.of_constr (whd_all env sigma c)) in + let (t, l) = Termops.decompose_app_vect sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind -> (ind, l) | _ -> raise Not_found @@ -466,7 +466,7 @@ let find_mrectype env sigma c = let find_rectype env sigma c = let open EConstr in - let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in + let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind (ind,u as indu) -> let (mib,mip) = Inductive.lookup_mind_specif env ind in @@ -478,7 +478,7 @@ let find_rectype env sigma c = let find_inductive env sigma c = let open EConstr in - let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in + let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite <> Decl_kinds.CoFinite -> @@ -488,7 +488,7 @@ let find_inductive env sigma c = let find_coinductive env sigma c = let open EConstr in - let (t, l) = decompose_app sigma (EConstr.of_constr (whd_all env sigma c)) in + let (t, l) = decompose_app sigma (whd_all env sigma c) in match EConstr.kind sigma t with | Ind ind when (fst (Inductive.lookup_mind_specif env (fst ind))).mind_finite == Decl_kinds.CoFinite -> @@ -503,7 +503,7 @@ let find_coinductive env sigma c = let is_predicate_explicitly_dep env sigma pred arsign = let rec srec env pval arsign = - let pv' = EConstr.of_constr (whd_all env sigma pval) in + let pv' = whd_all env sigma pval in match EConstr.kind sigma pv', arsign with | Lambda (na,t,b), (LocalAssum _)::arsign -> srec (push_rel_assum (na, t) env) b arsign |