diff options
| author | Maxime Dénès | 2019-04-05 12:18:49 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2019-04-10 15:41:45 +0200 |
| commit | 5af486406e366bf23558311a7367e573c617e078 (patch) | |
| tree | e2996582ca8eab104141dd75b82ac1777e53cb72 /pretyping/evarsolve.ml | |
| parent | f6dc8b19760aaf0cc14e6d9eb2d581ba1a05a762 (diff) | |
Remove calls to global env in Inductiveops
Diffstat (limited to 'pretyping/evarsolve.ml')
| -rw-r--r-- | pretyping/evarsolve.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml index 6d2d07d1dc..4a941a68b1 100644 --- a/pretyping/evarsolve.ml +++ b/pretyping/evarsolve.ml @@ -1203,17 +1203,17 @@ exception CannotProject of evar_map * EConstr.existential of subterms to eventually discard so as to be allowed to keep ti. *) -let rec is_constrainable_in top evd k (ev,(fv_rels,fv_ids) as g) t = +let rec is_constrainable_in top env evd k (ev,(fv_rels,fv_ids) as g) t = let f,args = decompose_app_vect evd t in match EConstr.kind evd f with | Construct ((ind,_),u) -> - let n = Inductiveops.inductive_nparams ind in + let n = Inductiveops.inductive_nparams env ind in if n > Array.length args then true (* We don't try to be more clever *) else let params = fst (Array.chop n args) in - Array.for_all (is_constrainable_in false evd k g) params - | Ind _ -> Array.for_all (is_constrainable_in false evd k g) args - | Prod (na,t1,t2) -> is_constrainable_in false evd k g t1 && is_constrainable_in false evd k g t2 + Array.for_all (is_constrainable_in false env evd k g) params + | Ind _ -> Array.for_all (is_constrainable_in false env evd k g) args + | Prod (na,t1,t2) -> is_constrainable_in false env evd k g t1 && is_constrainable_in false env evd k g t2 | Evar (ev',_) -> top || not (Evar.equal ev' ev) (*If ev' needed, one may also try to restrict it*) | Var id -> Id.Set.mem id fv_ids | Rel n -> n <= k || Int.Set.mem n fv_rels @@ -1238,7 +1238,7 @@ let has_constrainable_free_vars env evd aliases force k ev (fv_rels,fv_ids,let_r | None -> (* t is an instance for a proper variable; we filter it along *) (* the free variables allowed to occur *) - (not force || noccur_evar env evd ev t) && is_constrainable_in true evd k (ev,(fv_rels,fv_ids)) t + (not force || noccur_evar env evd ev t) && is_constrainable_in true env evd k (ev,(fv_rels,fv_ids)) t exception EvarSolvedOnTheFly of evar_map * EConstr.constr |