aboutsummaryrefslogtreecommitdiff
path: root/src/tac2intern.ml
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2017-09-06 22:47:44 +0200
committerPierre-Marie Pédrot2017-09-06 23:36:10 +0200
commit64a6ac3759b5d0ea635ff284606541b05c696996 (patch)
tree46461ca46923a81321a1715091072e30b9848354 /src/tac2intern.ml
parentf5ed96350ecc947ad4e55be9439cd0d30c68bde0 (diff)
Using higher-order representation for closures.
Diffstat (limited to 'src/tac2intern.ml')
-rw-r--r--src/tac2intern.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/tac2intern.ml b/src/tac2intern.ml
index d1a3e13cdb..2dcd8b8da3 100644
--- a/src/tac2intern.ml
+++ b/src/tac2intern.ml
@@ -654,7 +654,7 @@ let rec intern_rec env (loc, e) = match e with
let sch = Id.Map.find id env.env_var in
(GTacVar id, fresh_mix_type_scheme env sch)
| ArgArg (TacConstant kn) ->
- let { Tac2env.gdata_type = sch }, _ =
+ let { Tac2env.gdata_type = sch } =
try Tac2env.interp_global kn
with Not_found ->
CErrors.anomaly (str "Missing hardwired primitive " ++ KerName.print kn)