diff options
| author | Pierre-Marie Pédrot | 2020-07-13 15:02:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-08-06 12:33:58 +0200 |
| commit | 7126990e5b04d51927f414b277124c127fb14887 (patch) | |
| tree | aeffc105a7e498d1db244a30facbbfd09fab8c9d /engine/eConstr.ml | |
| parent | 8076de05c67a4dabc99233d8e2b81809c28794e4 (diff) | |
Actually use the default instance stored inside named_context_val.
Diffstat (limited to 'engine/eConstr.ml')
| -rw-r--r-- | engine/eConstr.ml | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/engine/eConstr.ml b/engine/eConstr.ml index 334c23c963..36297fe243 100644 --- a/engine/eConstr.ml +++ b/engine/eConstr.ml @@ -743,6 +743,9 @@ let match_named_context_val : match unsafe_eq with | Refl -> match_named_context_val +let identity_subst_val : named_context_val -> t list = + match unsafe_eq with Refl -> fun ctx -> ctx.env_named_var + let fresh_global ?loc ?rigid ?names env sigma reference = let (evd,t) = Evd.fresh_global ?loc ?rigid ?names env sigma reference in evd, t |