aboutsummaryrefslogtreecommitdiff
path: root/proofs/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/tacinterp.ml')
-rw-r--r--proofs/tacinterp.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index b037a4a310..32d96bce16 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -52,7 +52,7 @@ type value =
(* Signature for interpretation: val_interp and interpretation functions *)
and interp_sign =
- { evc : enamed_declarations;
+ { evc : Evd.evar_map;
env : Environ.env;
lfun : (identifier * value) list;
lmatch : (int * constr) list;