coq-community / paramcoq

Coq plugin for parametricity [maintainer=@proux01]
Other
44 stars 24 forks source link

Typo #96

Open SnarkBoojum opened 2 years ago

SnarkBoojum commented 2 years ago

In src/parametricity, you should s/environement/environment/g:

--- paramcoq.orig/src/parametricity.ml
+++ paramcoq/src/parametricity.ml
@@ -604,7 +604,7 @@
      compose_prod_assum (lift_rel_context (nfun * order) ft_R) (substl sub bk_R)) ftbk_R
   in

-  (* env_rec is the environement under fixpoints. *)
+  (* env_rec is the environment under fixpoints. *)
   let env_rec = push_rec_types (lna, tl, bl) env in
   (* n : fix index *)
   let process_body n =
@@ -705,7 +705,7 @@
      in
      compose_prod_assum (lift_rel_context (nfun * order) ft_R) (substl sub bk_R)) ftbk_R
   in
-  (* env_rec is the environement under fixpoints. *)
+  (* env_rec is the environment under fixpoints. *)
   let env_rec = push_rec_types (lna, tl, bl) env in
   (* n : fix index *)
   let process_body n =
@@ -1059,7 +1059,7 @@
     let env_arities =
       List.fold_left (fun env ind ->
         let typename = ind.mind_typename in
-        debug_string [`Inductive] (Printf.sprintf "Adding '%s' to the environement." (Names.Id.to_string typename));
+        debug_string [`Inductive] (Printf.sprintf "Adding '%s' to the environment." (Names.Id.to_string typename));
         let full_arity, cst =
            Inductive.constrained_type_of_inductive ((b, ind), inst)
         in
proux01 commented 2 years ago

@SnarkBoojum Indeed, please open a pull request.

SnarkBoojum commented 2 years ago

To make a pull request, I need to click around github to clone the repository, then clone it locally, apply the Debian patch, commit, push then click around github for a PR -- it's really overkill!