diff options
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/ppdecl_proof.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/decl_mode/ppdecl_proof.ml b/plugins/decl_mode/ppdecl_proof.ml index 5bd15b93fa..e8a8ac2267 100644 --- a/plugins/decl_mode/ppdecl_proof.ml +++ b/plugins/decl_mode/ppdecl_proof.ml @@ -77,7 +77,7 @@ and print_vars pconstr gtyp env sep _be _have vars = match st.st_label with Anonymous -> anomaly "anonymous variable" | Name id -> Environ.push_named (id,None,st.st_it) env in - let pr_sep = if sep then pr_coma () else mt () in + let pr_sep = if sep then pr_comma () else mt () in spc() ++ pr_sep ++ pr_statement pr_constr env st ++ print_vars pconstr gtyp nenv true _be _have rest @@ -143,7 +143,7 @@ let rec pr_bare_proof_instr _then _thus env = function str "given" ++ print_vars pr_constr _I env false false "given" hyps | Ptake witl -> str "take" ++ spc () ++ - prlist_with_sep pr_coma (pr_constr env) witl + prlist_with_sep pr_comma (pr_constr env) witl | Pdefine (id,args,body) -> str "define" ++ spc () ++ pr_id id ++ spc () ++ prlist_with_sep spc |