-
Notifications
You must be signed in to change notification settings - Fork 25
Open
Description
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
Metadata
Metadata
Assignees
Labels
No labels