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 /tactics/inv.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 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index d76c9a697..412954989 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -124,12 +124,10 @@ let make_inv_predicate env evd indf realargs id status concl = in let eq_term = eqdata.Coqlib.eq in let eq = Evarutil.evd_comb1 (Evd.fresh_global env) evd eq_term in - let eq = EConstr.of_constr eq in let eqn = applist (eq,[eqnty;lhs;rhs]) in let eqns = (Anonymous, lift n eqn) :: eqns in let refl_term = eqdata.Coqlib.refl in let refl_term = Evarutil.evd_comb1 (Evd.fresh_global env) evd refl_term in - let refl_term = EConstr.of_constr refl_term in let refl = mkApp (refl_term, [|eqnty; rhs|]) in let _ = Evarutil.evd_comb1 (Typing.type_of env) evd refl in let args = refl :: args in |