From 3a0b543af4ac99b29efdebe27b1d204d044a7bf0 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 31 Mar 2018 17:43:18 +0200 Subject: 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. --- plugins/firstorder/sequent.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/firstorder') diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 83fbc2d5d..7c612c0d8 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -197,7 +197,7 @@ let extend_with_ref_list env sigma l seq = let l = expand_constructor_hints l in let f gr (seq, sigma) = let sigma, c = Evd.fresh_global env sigma gr in - let sigma, typ= Typing.type_of env sigma (EConstr.of_constr c) in + let sigma, typ= Typing.type_of env sigma c in (add_formula env sigma Hyp gr typ seq, sigma) in List.fold_right f l (seq, sigma) -- cgit v1.2.3