diff options
| author | Maxime Dénès | 2018-10-09 16:45:34 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2018-10-26 13:31:29 +0200 |
| commit | 8361be1d785f8588d2d3c2a0df7a1d9239bae5a1 (patch) | |
| tree | b44c6f8bed7e8f4ea09807b1239ab6ee3676aeeb /interp | |
| parent | e2096b9e6048bbab5c6da279bab3c3a719dc237f (diff) | |
Remove a few circumvolutions around parameters of inductive entries
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/discharge.ml | 11 |
1 files changed, 1 insertions, 10 deletions
diff --git a/interp/discharge.ml b/interp/discharge.ml index 0e44a8b467..21b2e85e8f 100644 --- a/interp/discharge.ml +++ b/interp/discharge.ml @@ -8,8 +8,6 @@ (* * (see LICENSE file for the text of the license) *) (************************************************************************) -open Names -open CErrors open Util open Term open Constr @@ -17,17 +15,10 @@ open Vars open Declarations open Cooking open Entries -open Context.Rel.Declaration (********************************) (* Discharging mutual inductive *) -let detype_param = - function - | LocalAssum (Name id, p) -> id, LocalAssumEntry p - | LocalDef (Name id, p,_) -> id, LocalDefEntry p - | _ -> anomaly (Pp.str "Unnamed inductive local variable.") - (* Replace Var(y1)..Var(yq):C1..Cq |- Ij:Bj @@ -57,7 +48,7 @@ let abstract_inductive decls nparamdecls inds = (* To be sure to be the same as before, should probably be moved to process_inductive *) let params' = let (_,arity,_,_,_) = List.hd inds' in let (params,_) = decompose_prod_n_assum nparamdecls' arity in - List.map detype_param params + params in let ind'' = List.map |