diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 16:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-03-17 21:08:26 +0100 |
| commit | 4b2cdf733df6dc23247b078679e71da98e54f5cc (patch) | |
| tree | ac05560456999b14a897e1701ae6678ab5c6e6b7 /grammar | |
| parent | 4d13842869647790c9bd3084dce672fee7b648a1 (diff) | |
Removing the special status of generic entries defined by Coq itself.
The ARGUMENT EXTEND macro was discriminating between parsing entries known
statically, i.e. defined in Pcoq and unknown entires. Although simplifying
a bit the life of the plugin writer, it made actual interpretation difficult
to predict and complicated the code of the ARGUMENT EXTEND macro.
After this patch, all parsing entries and generic arguments used in an
ARGUMENT EXTEND macro must be reachable by the ML code. This requires adding
a few more "open Pcoq.X" and "open Constrarg" here and there.
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/argextend.ml4 | 7 | ||||
| -rw-r--r-- | grammar/q_util.ml4 | 15 |
2 files changed, 2 insertions, 20 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4 index 57ae357de..41e94914e 100644 --- a/grammar/argextend.ml4 +++ b/grammar/argextend.ml4 @@ -23,12 +23,7 @@ let qualified_name loc s = let (name, path) = CList.sep_last path in qualified_name loc path name -let mk_extraarg loc s = - try - let name = Genarg.get_name0 s in - qualified_name loc name - with Not_found -> - <:expr< $lid:"wit_"^s$ >> +let mk_extraarg loc s = <:expr< $lid:"wit_"^s$ >> let rec make_wit loc = function | ListArgType t -> <:expr< Genarg.wit_list $make_wit loc t$ >> diff --git a/grammar/q_util.ml4 b/grammar/q_util.ml4 index 1848bf85f..3946d5d2b 100644 --- a/grammar/q_util.ml4 +++ b/grammar/q_util.ml4 @@ -47,15 +47,6 @@ let mlexpr_of_option f = function let mlexpr_of_ident id = <:expr< Names.Id.of_string $str:id$ >> -let repr_entry e = - let entry u = - let _ = Pcoq.get_entry u e in - Some (Entry.univ_name u, e) - in - try entry Pcoq.uprim with Not_found -> - try entry Pcoq.uconstr with Not_found -> - try entry Pcoq.utactic with Not_found -> None - let rec mlexpr_of_prod_entry_key = function | Extend.Ulist1 s -> <:expr< Pcoq.Alist1 $mlexpr_of_prod_entry_key s$ >> | Extend.Ulist1sep (s,sep) -> <:expr< Pcoq.Alist1sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> @@ -63,11 +54,7 @@ let rec mlexpr_of_prod_entry_key = function | Extend.Ulist0sep (s,sep) -> <:expr< Pcoq.Alist0sep $mlexpr_of_prod_entry_key s$ $str:sep$ >> | Extend.Uopt s -> <:expr< Pcoq.Aopt $mlexpr_of_prod_entry_key s$ >> | Extend.Umodifiers s -> <:expr< Pcoq.Amodifiers $mlexpr_of_prod_entry_key s$ >> - | Extend.Uentry e -> - begin match repr_entry e with - | None -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> - | Some (u, s) -> <:expr< Pcoq.Aentry (Entry.unsafe_of_name ($str:u$, $str:s$)) >> - end + | Extend.Uentry e -> <:expr< Pcoq.Aentry (Pcoq.name_of_entry $lid:e$) >> | Extend.Uentryl (e, l) -> (** Keep in sync with Pcoq! *) assert (CString.equal e "tactic"); |