diff options
author | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 13:07:53 +0100 |
---|---|---|
committer | Maxime Dénès <mail@maximedenes.fr> | 2018-02-12 13:07:53 +0100 |
commit | 284869d016607fad339ea4d06bf1433c6ec23672 (patch) | |
tree | 1cae1f278186bb0aa9643fb57ca9af0eb029672f /kernel/reduction.ml | |
parent | 52d666a7a83e4023d9f5cd7324ed81c7f7926156 (diff) | |
parent | 42610a4659cf35e6a005d79eec273c606bdf87dd (diff) |
Merge PR #1082: Fixing Print for inductive types with let-in in parameters
Diffstat (limited to 'kernel/reduction.ml')
-rw-r--r-- | kernel/reduction.ml | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 159d2ea66..da7042713 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -882,6 +882,18 @@ let hnf_prod_app env t n = let hnf_prod_applist env t nl = List.fold_left (hnf_prod_app env) t nl +let hnf_prod_applist_assum env n c l = + let rec app n subst t l = + if Int.equal n 0 then + if l == [] then substl subst t + else anomaly (Pp.str "Too many arguments.") + else match kind (whd_allnolet env t), l with + | Prod(_,_,c), arg::l -> app (n-1) (arg::subst) c l + | LetIn(_,b,_,c), _ -> app (n-1) (substl subst b::subst) c l + | _, [] -> anomaly (Pp.str "Not enough arguments.") + | _ -> anomaly (Pp.str "Not enough prod/let's.") in + app n [] c l + (* Dealing with arities *) let dest_prod env = |