diff options
| author | ppedrot | 2012-10-04 11:53:07 +0000 |
|---|---|---|
| committer | ppedrot | 2012-10-04 11:53:07 +0000 |
| commit | 5b6582f8d47975f6f4f394cf44a1c65c799d43ff (patch) | |
| tree | e1be15920daf8b2e5ae788f57e772e79ddaacd30 /plugins/decl_mode | |
| parent | 621625757d04bdb19075d92e764749d0a1393ce3 (diff) | |
Moved Compat to parsing. This permits to break the dependency of the
kernel on CAMLP4/5 structures, and consequently should also erase
such structures from vo files.
This modification requires some code duplication, mainly while
reimplementing our own location data type. This is chiefly visible
in the ml4 files, where CAMLP4/5 locations must be manually converted
to our locations with an explicit (!@) cast operator.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15847 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4 index e8e81c472c..a3052320cf 100644 --- a/plugins/decl_mode/g_decl_mode.ml4 +++ b/plugins/decl_mode/g_decl_mode.ml4 @@ -10,6 +10,7 @@ (* arnaud: veiller à l'aspect tutorial des commentaires *) +open Compat open Pp open Tok open Decl_expr @@ -189,7 +190,7 @@ GLOBAL: proof_instr; statement : [[ i=ident ; ":" ; c=constr -> {st_label=Name i;st_it=c} | i=ident -> {st_label=Anonymous; - st_it=Constrexpr.CRef (Libnames.Ident (loc, i))} + st_it=Constrexpr.CRef (Libnames.Ident (!@loc, i))} | c=constr -> {st_label=Anonymous;st_it=c} ]]; constr_or_thesis : @@ -202,7 +203,7 @@ GLOBAL: proof_instr; | [ i=ident ; ":" ; cot=constr_or_thesis -> {st_label=Name i;st_it=cot} | i=ident -> {st_label=Anonymous; - st_it=This (Constrexpr.CRef (Libnames.Ident (loc, i)))} + st_it=This (Constrexpr.CRef (Libnames.Ident (!@loc, i)))} | c=constr -> {st_label=Anonymous;st_it=This c} ] ]; |