From 8beca748d992cd08e2dd7448c8b28dadbcea4a16 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 26 Nov 2016 01:09:11 +0100 Subject: Cleaning up interfaces. We make mli files look to what they were looking before the move to EConstr by opening this module. --- pretyping/pretyping.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping/pretyping.ml') diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index f76f608d0..6b6800ac6 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -61,7 +61,7 @@ type ltac_var_map = { ltac_genargs : unbound_ltac_var_map; } type glob_constr_ltac_closure = ltac_var_map * glob_constr -type pure_open_constr = evar_map * Constr.constr +type pure_open_constr = evar_map * EConstr.constr (************************************************************************) (* This concerns Cases *) -- cgit v1.2.3