wip

src/coq_elpi_builtins_synterp.ml

@@ -360,7 +360,7 @@ module SynterpAction = struct
   let pop case state =
     State.update_return read state (function
       | x :: xs -> Vernacstate.Synterp.unfreeze x.resulting_state; xs, x.action
-      | _ -> synterp_interp_error Pp.(strbrk ("The elpi program did perform no (more) actions during the parsing phase (aka synterp), while during the execution phase (aka interp) it tried to perform a " ^ case ^ " action. " ^ common_err)))
+      | _ -> synterp_interp_error Pp.(hov 0 (strbrk ("The command did perform no (more) actions during the parsing phase (aka synterp), while during the execution phase (aka interp) it tried to perform a") ++ spc() ++ str case ++ spc() ++ str "action." ++ spc() ++ strbrk common_err)))
 
   let pop_opt state =
     State.update_return read state (function
@@ -373,15 +373,15 @@ module SynterpAction = struct
     match action with
     | BeginModule((name,_,_),binders_ast,ty) ->
         if Global.sections_are_opened () then
-          err Pp.(str"This elpi code cannot be run within a section since it opens a module");
+          err Pp.(str"This code cannot be run within a section since it opens a module");
         let id = Id.of_string name in
         let mp = Declaremods.Interp.start_module None id binders_ast ty in
         let loc = to_coq_loc @@ State.get invocation_site_loc state in
         Dumpglob.dump_moddef ~loc mp "mod";
         None
     | BeginModuleType((name,_),binders_ast,ty) ->
         if Global.sections_are_opened () then
-          err Pp.(str"This elpi code cannot be run within a section since it opens a module");
+          err Pp.(str"This code cannot be run within a section since it opens a module");
         let id = Id.of_string name in
         let mp = Declaremods.Interp.start_modtype id binders_ast ty in
         let loc = to_coq_loc @@ State.get invocation_site_loc state in
@@ -444,11 +444,11 @@ module SynterpAction = struct
 
   let wrong_synterp_action x a =
     synterp_interp_error Pp.(str "The elpi program did perform" ++ spc () ++ pp_action a ++ spc () ++
-      str" at parsing time, while at run time it tried to perform" ++ spc () ++ str x ++ str(". "^common_err))
+      str" at parsing time, while at execution time it tried to perform" ++ spc () ++ str x ++ str(". "^common_err))
   let check_inconsistent_synterp_action eq ppx ppy x y a =
     if not (eq x y) then
       synterp_interp_error Pp.(str "The elpi program did perform" ++ spc () ++ pp_action a ++ spc () ++
-        str" at parsing time and runtime, but on different inputs" ++ spc () ++ ppx x ++ str " != " ++ ppy y ++ str(". "^common_err))
+        str" at parsing time and execution, but on different inputs" ++ spc () ++ ppx x ++ str " != " ++ ppy y ++ str(". "^common_err))
 
   let check_inconsistent_synterp_action_string =
     check_inconsistent_synterp_action (=) Pp.str Pp.str

src/coq_elpi_vernacular.ml

@@ -589,7 +589,7 @@ module Interp = struct
             match synterp_left with
             | [] -> Vernacstate.Synterp.unfreeze final_synterp_state
             | x :: _ ->
-                err Pp.(strbrk"The interpretation phase did not consume all the parsing time effects. Next in the queue is " ++ Coq_elpi_builtins_synterp.SynterpAction.pp x)
+                err Pp.(strbrk"The execution phase did not consume all the parse time actions. Next in the queue is " ++ Coq_elpi_builtins_synterp.SynterpAction.pp x)
         with
         | Coq_elpi_builtins_synterp.SynterpAction.Error x when syndata = None ->
             err Pp.(x ++ missing_synterp)