diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-03-31 17:43:18 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2018-04-13 12:57:39 +0200 |
| commit | 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 (patch) | |
| tree | e1f926647c686a559b045654924a50535afa25c0 /pretyping/coercion.ml | |
| parent | f3b84cf63c242623bdcccd30c536e55983971da5 (diff) | |
Evar maps contain econstrs.
We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.
Diffstat (limited to 'pretyping/coercion.ml')
| -rw-r--r-- | pretyping/coercion.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml index 04cb6a59f..6dc3687a0 100644 --- a/pretyping/coercion.ml +++ b/pretyping/coercion.ml @@ -251,7 +251,7 @@ and coerce ?loc env evdref (x : EConstr.constr) (y : EConstr.constr) let (n, dom, rng) = destLambda !evdref t in if isEvar !evdref dom then let (domk, args) = destEvar !evdref dom in - evdref := define domk (EConstr.Unsafe.to_constr a) !evdref; + evdref := define domk a !evdref; else (); t, rng | _ -> raise NoSubtacCoercion |