From bf5f0520cf105afb048c6eac5d6de1d3e1a719df Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Thu, 4 Apr 2019 21:06:34 +0200
Subject: Remove one call to Global.env in Detyping

One other call still remains, but will require to refactor some
section-handling code.
---
 pretyping/patternops.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/patternops.mli')

diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index 36317b3acf..90a536e780 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -21,7 +21,7 @@ val constr_pattern_eq : constr_pattern -> constr_pattern -> bool
 
 val occur_meta_pattern : constr_pattern -> bool
 
-val subst_pattern : substitution -> constr_pattern -> constr_pattern
+val subst_pattern : Environ.env -> substitution -> constr_pattern -> constr_pattern
 
 val noccurn_pattern : int -> constr_pattern -> bool
 
-- 
cgit v1.2.3