diff options
Diffstat (limited to 'plugins')
| -rw-r--r-- | plugins/decl_mode/g_decl_mode.ml4 | 5 | ||||
| -rw-r--r-- | plugins/firstorder/g_ground.ml4 | 2 | ||||
| -rw-r--r-- | plugins/funind/g_indfun.ml4 | 3 |
3 files changed, 6 insertions, 4 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} ] ]; diff --git a/plugins/firstorder/g_ground.ml4 b/plugins/firstorder/g_ground.ml4 index 3039324847..160ca1b4c0 100644 --- a/plugins/firstorder/g_ground.ml4 +++ b/plugins/firstorder/g_ground.ml4 @@ -104,7 +104,7 @@ open Genarg open Ppconstr open Printer let pr_firstorder_using_raw _ _ _ = prlist_with_sep pr_comma pr_reference -let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (Loc.pr_located pr_global)) +let pr_firstorder_using_glob _ _ _ = prlist_with_sep pr_comma (pr_or_var (fun x -> (pr_global (snd x)))) let pr_firstorder_using_typed _ _ _ = prlist_with_sep pr_comma pr_global ARGUMENT EXTEND firstorder_using diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4 index 77c6dc4938..0dceecf4f1 100644 --- a/plugins/funind/g_indfun.ml4 +++ b/plugins/funind/g_indfun.ml4 @@ -6,6 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) (*i camlp4deps: "grammar/grammar.cma" i*) +open Compat open Util open Term open Names @@ -145,7 +146,7 @@ GEXTEND Gram GLOBAL: function_rec_definition_loc ; function_rec_definition_loc: - [ [ g = Vernac.rec_definition -> loc, g ]] + [ [ g = Vernac.rec_definition -> !@loc, g ]] ; END |