diff options
| author | Talia Ringer | 2019-05-22 16:09:51 -0400 |
|---|---|---|
| committer | Talia Ringer | 2019-05-22 16:09:51 -0400 |
| commit | 577db38704896c75d1db149f6b71052ef47202be (patch) | |
| tree | 946afdb361fc9baaa696df7891d0ddc03a4a8594 /kernel/environ.ml | |
| parent | 7eefc0b1db614158ed1b322f8c6e5601e3995113 (diff) | |
| parent | e9a5fe993ba36e22316ac9f6ef0564f38a3eb4f9 (diff) | |
Merge remote-tracking branch 'origin/master' into stm+doc_hook
Diffstat (limited to 'kernel/environ.ml')
| -rw-r--r-- | kernel/environ.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 97c9f8654a..05f342a82a 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -46,7 +46,7 @@ type link_info = | LinkedInteractive of string | NotLinked -type constant_key = constant_body * (link_info ref * key) +type constant_key = Opaqueproof.opaque constant_body * (link_info ref * key) type mind_key = mutual_inductive_body * link_info ref @@ -187,7 +187,7 @@ let match_named_context_val c = match c.env_named_ctx with let map_named_val f ctxt = let open Context.Named.Declaration in let fold accu d = - let d' = map_constr f d in + let d' = f d in let accu = if d == d' then accu else Id.Map.modify (get_id d) (fun _ (_, v) -> (d', v)) accu |