diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-11-20 00:27:08 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-02-14 17:30:21 +0100 |
| commit | 372b092aea6d077fe0a82eac74d742da8998c7ad (patch) | |
| tree | 4345b93e0ba0bb5570624ef9f09840d424962111 /tactics/auto.ml | |
| parent | 34e86e839be251717db96f1f5969d7724ab43097 (diff) | |
Auto API using EConstr.
Diffstat (limited to 'tactics/auto.ml')
| -rw-r--r-- | tactics/auto.ml | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml index 2423ea878..c34f9dd92 100644 --- a/tactics/auto.ml +++ b/tactics/auto.ml @@ -6,14 +6,15 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* -*) +module CVars = Vars + open Pp open Util open CErrors open Names open Vars open Termops +open EConstr open Environ open Tacmach open Genredexpr @@ -83,8 +84,8 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl = if poly then (** Refresh the instance of the hint *) let (subst, ctx) = Universes.fresh_universe_context_set_instance ctx in - let map c = Vars.subst_univs_level_constr subst c in - let emap c = EConstr.Vars.subst_univs_level_constr subst c in + let map c = CVars.subst_univs_level_constr subst c in + let emap c = Vars.subst_univs_level_constr subst c in let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in (** Only metas are mentioning the old universes. *) let clenv = { |