diff options
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index 1aba2bbdd1..2bd0c06d6d 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -994,12 +994,14 @@ let rec strip_outer_cast sigma c = match EConstr.kind sigma c with (* flattens application lists throwing casts in-between *) let collapse_appl sigma c = match EConstr.kind sigma c with | App (f,cl) -> + if EConstr.isCast sigma f then let rec collapse_rec f cl2 = match EConstr.kind sigma (strip_outer_cast sigma f) with | App (g,cl1) -> collapse_rec g (Array.append cl1 cl2) | _ -> EConstr.mkApp (f,cl2) in collapse_rec f cl + else c | _ -> c (* First utilities for avoiding telescope computation for subst_term *) @@ -1145,9 +1147,6 @@ let is_template_polymorphic env sigma f = | Ind (ind, u) -> if not (EConstr.EInstance.is_empty u) then false else Environ.template_polymorphic_ind ind env - | Const (cst, u) -> - if not (EConstr.EInstance.is_empty u) then false - else Environ.template_polymorphic_constant cst env | _ -> false let base_sort_cmp pb s0 s1 = |