diff options
Diffstat (limited to 'toplevel/discharge.ml')
| -rw-r--r-- | toplevel/discharge.ml | 13 |
1 files changed, 8 insertions, 5 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index 61a6e10948..ffa11679c2 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -14,14 +14,17 @@ open Vars open Entries open Declarations open Cooking +open Entries +open Context.Rel.Declaration (********************************) (* Discharging mutual inductive *) -let detype_param = function - | (Name id,None,p) -> id, LocalAssum p - | (Name id,Some p,_) -> id, LocalDef p - | (Anonymous,_,_) -> anomaly (Pp.str "Unnamed inductive local variable") +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 @@ -52,7 +55,7 @@ let abstract_inductive hyps nparams 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 nparams' arity in - List.map detype_param params + List.map detype_param params in let ind'' = List.map |