diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-12 15:30:28 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-12 15:30:28 +0000 |
| commit | a885a2148e4d45606c654145db5d859c4d6a223b (patch) | |
| tree | 5feb549d45868e5eab7762891d0e7dc46f4e7760 /plugins/decl_mode/ppdecl_proof.ml | |
| parent | d30267620672a939f56fb9d6e161070bbb1112a6 (diff) | |
Fixing spelling: pr_coma -> pr_comma
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13119 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/decl_mode/ppdecl_proof.ml')
| -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 5bd15b93f..e8a8ac226 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 |