diff options
Diffstat (limited to 'parsing/egramcoq.ml')
| -rw-r--r-- | parsing/egramcoq.ml | 5 |
1 files changed, 0 insertions, 5 deletions
diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 712d10a96..6940fd6fb 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -10,7 +10,6 @@ open CErrors open Util open Pcoq open Constrexpr -open Notation open Notation_term open Extend open Libnames @@ -80,10 +79,6 @@ let create_pos = function | None -> Extend.First | Some lev -> Extend.After (constr_level lev) -type gram_level = - gram_position option * gram_assoc option * string option * - (** for reinitialization: *) gram_reinit option - let find_position_gen current ensure assoc lev = match lev with | None -> |