diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-01 02:36:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-01 20:19:53 +0200 |
| commit | 7babf0d42af11f5830bc157a671bd81b478a4f02 (patch) | |
| tree | 428ee1f95355ee5e11c19e12d538e37cc5a81f6c /engine/termops.ml | |
| parent | 3df2431a80f9817ce051334cb9c3b1f465bffb60 (diff) | |
Using delayed universe instances in EConstr.
The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
Diffstat (limited to 'engine/termops.ml')
| -rw-r--r-- | engine/termops.ml | 14 |
1 files changed, 9 insertions, 5 deletions
diff --git a/engine/termops.ml b/engine/termops.ml index a67916345..64f4c6dc5 100644 --- a/engine/termops.ml +++ b/engine/termops.ml @@ -1150,7 +1150,7 @@ let global_of_constr sigma c = | Const (c, u) -> ConstRef c, u | Ind (i, u) -> IndRef i, u | Construct (c, u) -> ConstructRef c, u - | Var id -> VarRef id, Univ.Instance.empty + | Var id -> VarRef id, EConstr.EInstance.empty | _ -> raise Not_found let is_global sigma c t = @@ -1169,8 +1169,12 @@ let isGlobalRef sigma c = let is_template_polymorphic env sigma f = match EConstr.kind sigma f with - | Ind ind -> Environ.template_polymorphic_pind ind env - | Const c -> Environ.template_polymorphic_pconstant c env + | 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 = @@ -1453,8 +1457,8 @@ let global_app_of_constr sigma c = | Const (c, u) -> (ConstRef c, u), None | Ind (i, u) -> (IndRef i, u), None | Construct (c, u) -> (ConstructRef c, u), None - | Var id -> (VarRef id, Instance.empty), None - | Proj (p, c) -> (ConstRef (Projection.constant p), Instance.empty), Some c + | Var id -> (VarRef id, EConstr.EInstance.empty), None + | Proj (p, c) -> (ConstRef (Projection.constant p), EConstr.EInstance.empty), Some c | _ -> raise Not_found let prod_applist sigma c l = |