diff options
| author | Enrico Tassi | 2015-02-23 17:14:05 +0100 |
|---|---|---|
| committer | Enrico Tassi | 2015-02-23 17:14:05 +0100 |
| commit | e87ca456fb4cbe54f09e13f1e20d504d2699ac2b (patch) | |
| tree | 41b358ee2deb7c614e39f7db27368f9626c19778 /plugins/funind/invfun.ml | |
| parent | 28781f3fd6ae6e7f281f906721e8a028679ca089 (diff) | |
| parent | df2f50db3703b4f7f88f00ac382c7f3f1efaceb3 (diff) | |
Merge branch 'v8.5' into trunk
Diffstat (limited to 'plugins/funind/invfun.ml')
| -rw-r--r-- | plugins/funind/invfun.ml | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml index b9d7e0d909..0ee8877082 100644 --- a/plugins/funind/invfun.ml +++ b/plugins/funind/invfun.ml @@ -45,7 +45,7 @@ let pr_with_bindings prc prlc (c,bl) = let pr_constr_with_binding prc (c,bl) : Pp.std_ppcmds = pr_with_bindings prc prc (c,bl) -(* The local debuging mechanism *) +(* The local debugging mechanism *) (* let msgnl = Pp.msgnl *) let observe strm = @@ -255,12 +255,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let f_principle,princ_type = schemes.(i) in let princ_type = nf_zeta princ_type in let princ_infos = Tactics.compute_elim_sig princ_type in - (* The number of args of the function is then easilly computable *) + (* The number of args of the function is then easily computable *) let nb_fun_args = nb_prod (pf_concl g) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in - (* Since we cannot ensure that the funcitonnal principle is defined in the - environement and due to the bug #1174, we will need to pose the principle + (* Since we cannot ensure that the functional principle is defined in the + environment and due to the bug #1174, we will need to pose the principle using a name *) let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in @@ -522,12 +522,12 @@ let prove_fun_correct functional_induction funs_constr graphs_constr schemes lem let f_principle,princ_type = schemes.(i) in let princ_type = nf_zeta princ_type in let princ_infos = Tactics.compute_elim_sig princ_type in - (* The number of args of the function is then easilly computable *) + (* The number of args of the function is then easily computable *) let nb_fun_args = nb_prod (pf_concl g) - 2 in let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in let ids = args_names@(pf_ids_of_hyps g) in - (* Since we cannot ensure that the funcitonnal principle is defined in the - environement and due to the bug #1174, we will need to pose the principle + (* Since we cannot ensure that the functional principle is defined in the + environment and due to the bug #1174, we will need to pose the principle using a name *) let principle_id = Namegen.next_ident_away_in_goal (Id.of_string "princ") ids in |