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 /plugins/ssr/ssrelim.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 'plugins/ssr/ssrelim.ml')
| -rw-r--r-- | plugins/ssr/ssrelim.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ssr/ssrelim.ml b/plugins/ssr/ssrelim.ml index 717657a24..de8ffb976 100644 --- a/plugins/ssr/ssrelim.ml +++ b/plugins/ssr/ssrelim.ml @@ -356,7 +356,7 @@ let ssrelim ?(ind=ref None) ?(is_case=false) deps what ?elim eqid elim_intro_tac let ev = List.fold_left Evar.Set.union Evar.Set.empty patterns_ev in let ty_ev = Evar.Set.fold (fun i e -> let ex = i in - let i_ty = EConstr.of_constr (Evd.evar_concl (Evd.find (project gl) ex)) in + let i_ty = Evd.evar_concl (Evd.find (project gl) ex) in Evar.Set.union e (evars_of_term i_ty)) ev Evar.Set.empty in let inter = Evar.Set.inter ev ty_ev in |