diff options
| author | Pierre-Marie Pédrot | 2015-02-17 16:28:48 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-02-17 16:28:48 +0100 |
| commit | df3d820b45695e273515f8d7cf7c0345c7d574c5 (patch) | |
| tree | 6b0545cd4bea33e7021b58c551decf02f2af5025 | |
| parent | 8c0bc2f5e51b6037868a4dcab612390e67136be0 (diff) | |
Fixing bug #4053.
| -rw-r--r-- | library/assumptions.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/library/assumptions.ml b/library/assumptions.ml index 04ee14fb53..ab07b3647e 100644 --- a/library/assumptions.ml +++ b/library/assumptions.ml @@ -205,7 +205,8 @@ let assumptions ?(add_opaque=false) ?(add_transparent=false) st (* t *) = | Fix (_,(_, e1_array, e2_array)) | CoFix (_,(_,e1_array, e2_array)) -> (iter_array e1_array) ** (iter_array e2_array) | Const (kn,_) -> do_memoize_kn kn - | _ -> identity2 (* closed atomic types + rel *) + | Proj (_, e) -> iter e + | Rel _ | Sort _ | Ind _ | Construct _ -> identity2 and iter_array a = Array.fold_right (fun e f -> (iter e)**f) a identity2 in iter t s acc |