diff options
author | 2010-05-19 15:29:48 +0000 | |
---|---|---|
committer | 2010-05-19 15:29:48 +0000 | |
commit | 1b089eb0231b4bd6d4cafb30f9e051bb53665978 (patch) | |
tree | 489e0f8ce7b4a80db388c63219b9cf4380b7f185 /tactics/extraargs.mli | |
parent | 259dde7928696593c2d3c6de474f5cf50fa4417d (diff) |
Add (almost) compatibility with camlp4, without breaking support for camlp5
The choice between camlp4/5 is done during configure with flags
-usecamlp5 (default for the moment) vs. -usecamlp4.
Currently, to have a full camlp4 compatibility, you need to change
all "EXTEND" and "GEXTEND Gram" into "EXTEND Gram", and change "EOI"
into "`EOI" in grammar entries. I've a sed script that does that
(actually the converse), but I prefer to re-think it and check a few
things before branching this sed into the build mechanism.
lib/compat.ml4 is heavily used to hide incompatibilities between camlp4/5
and try to propose a common interface (cf LexerSig / GrammarSig).
A few incompatible quotations have been turned into underlying code
manually, in order to make the IFDEF CAMLP5 THEN ... ELSE ... END
parsable by both camlp4 and 5. See in particular the fate of
<:str_item< declare ... end >>
Stdpp isn't used anymore, but rather Ploc (hidden behind local module Loc).
This forces to use camlp5 > 5.01.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13019 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/extraargs.mli')
-rw-r--r-- | tactics/extraargs.mli | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli index ffa1bd747..2c750be36 100644 --- a/tactics/extraargs.mli +++ b/tactics/extraargs.mli @@ -16,15 +16,15 @@ open Rawterm val rawwit_orient : bool raw_abstract_argument_type val wit_orient : bool typed_abstract_argument_type -val orient : bool Pcoq.Gram.Entry.e +val orient : bool Pcoq.Gram.entry -val occurrences : (int list or_var) Pcoq.Gram.Entry.e +val occurrences : (int list or_var) Pcoq.Gram.entry val rawwit_occurrences : (int list or_var) raw_abstract_argument_type val wit_occurrences : (int list) typed_abstract_argument_type val rawwit_raw : constr_expr raw_abstract_argument_type val wit_raw : (Tacinterp.interp_sign * rawconstr) typed_abstract_argument_type -val raw : constr_expr Pcoq.Gram.Entry.e +val raw : constr_expr Pcoq.Gram.entry type 'id gen_place= ('id * hyp_location_flag,unit) location @@ -33,17 +33,17 @@ type place = identifier gen_place val rawwit_hloc : loc_place raw_abstract_argument_type val wit_hloc : place typed_abstract_argument_type -val hloc : loc_place Pcoq.Gram.Entry.e +val hloc : loc_place Pcoq.Gram.entry -val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.Entry.e +val in_arg_hyp: (Names.identifier Util.located list option * bool) Pcoq.Gram.entry val rawwit_in_arg_hyp : (Names.identifier Util.located list option * bool) raw_abstract_argument_type val wit_in_arg_hyp : (Names.identifier list option * bool) typed_abstract_argument_type val raw_in_arg_hyp_to_clause : (Names.identifier Util.located list option * bool) -> Tacticals.clause val glob_in_arg_hyp_to_clause : (Names.identifier list option * bool) -> Tacticals.clause -val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.Entry.e +val by_arg_tac : Tacexpr.raw_tactic_expr option Pcoq.Gram.entry val rawwit_by_arg_tac : raw_tactic_expr option raw_abstract_argument_type val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type @@ -51,6 +51,6 @@ val wit_by_arg_tac : glob_tactic_expr option typed_abstract_argument_type (** Spiwack: Primitive for retroknowledge registration *) -val retroknowledge_field : Retroknowledge.field Pcoq.Gram.Entry.e +val retroknowledge_field : Retroknowledge.field Pcoq.Gram.entry val rawwit_retroknowledge_field : Retroknowledge.field raw_abstract_argument_type val wit_retroknowledge_field : Retroknowledge.field typed_abstract_argument_type |