File tree Expand file tree Collapse file tree 1 file changed +3
-2
lines changed
Expand file tree Collapse file tree 1 file changed +3
-2
lines changed Original file line number Diff line number Diff line change 11(* Distributed under the terms of the MIT license. *)
22From Coq Require Import Utf8 Program .
3- From MetaCoq Require Import config utils BasicAst.
3+ From MetaCoq.Utils Require Import utils.
4+ From MetaCoq.Common Require Import config BasicAst.
45From MetaCoq.PCUIC Require PCUICWcbvEval.
56From MetaCoq.Erasure Require Import EAst EAstUtils ELiftSubst ECSubst EReflect EGlobalEnv
67 EWellformed EWcbvEval.
@@ -671,7 +672,7 @@ Local Notation "'⊩' v ~ s" := (represents_value v s) (at level 50).
671672Local Hint Constructors represents : core.
672673Local Hint Constructors represents_value : core.
673674
674- From MetaCoq Require Import bytestring MCString.
675+ From MetaCoq.Utils Require Import bytestring MCString.
675676Require Import BinaryString.
676677Import String.
677678
You can’t perform that action at this time.
0 commit comments