summaryrefslogtreecommitdiff
path: root/plugins/funind
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/funind')
-rw-r--r--plugins/funind/Recdef.v2
-rw-r--r--plugins/funind/functional_principles_proofs.mli2
-rw-r--r--plugins/funind/functional_principles_types.mli2
-rw-r--r--plugins/funind/g_indfun.ml42
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--plugins/funind/invfun.ml2
-rw-r--r--plugins/funind/merge.ml2
-rw-r--r--plugins/funind/recdef.ml14
8 files changed, 14 insertions, 14 deletions
diff --git a/plugins/funind/Recdef.v b/plugins/funind/Recdef.v
index a63941f0..e4433247 100644
--- a/plugins/funind/Recdef.v
+++ b/plugins/funind/Recdef.v
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/functional_principles_proofs.mli b/plugins/funind/functional_principles_proofs.mli
index 61fce267..34ce6696 100644
--- a/plugins/funind/functional_principles_proofs.mli
+++ b/plugins/funind/functional_principles_proofs.mli
@@ -8,7 +8,7 @@ val prove_princ_for_struct :
val prove_principle_for_gen :
- constant*constant*constant -> (* name of the function, the fonctionnal and the fixpoint equation *)
+ constant*constant*constant -> (* name of the function, the functional and the fixpoint equation *)
constr option ref -> (* a pointer to the obligation proofs lemma *)
bool -> (* is that function uses measure *)
int -> (* the number of recursive argument *)
diff --git a/plugins/funind/functional_principles_types.mli b/plugins/funind/functional_principles_types.mli
index bc082f07..3fa2644c 100644
--- a/plugins/funind/functional_principles_types.mli
+++ b/plugins/funind/functional_principles_types.mli
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 045beb37..a15e46bf 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 1b12cd42..5d92fca5 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -681,7 +681,7 @@ and build_entry_lc_from_case env funname make_discr
let case_resl =
List.fold_right
(fun (case_arg,_) ctxt_argsl ->
- let arg_res = build_entry_lc env funname avoid case_arg in
+ let arg_res = build_entry_lc env funname ctxt_argsl.to_avoid case_arg in
combine_results combine_args arg_res ctxt_argsl
)
el
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d9794014..a800c186 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index e3455e77..87d7ca76 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 5d41ec72..065d0fe5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1,6 +1,6 @@
(************************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
-(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015 *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
@@ -203,7 +203,7 @@ let (declare_f : Id.t -> logical_kind -> constr list -> global_reference -> glob
-(* Debuging mechanism *)
+(* Debugging mechanism *)
let debug_queue = Stack.create ()
let rec print_debug_queue b e =
@@ -291,9 +291,9 @@ let tclUSER_if_not_mes concl_tac is_mes names_to_suppress =
-(* Travelling term.
+(* Traveling term.
Both definitions of [f_terminate] and [f_equation] use the same generic
- travelling mechanism.
+ traveling mechanism.
*)
(* [check_not_nested forbidden e] checks that [e] does not contains any variable
@@ -327,7 +327,7 @@ let check_not_nested forbidden e =
with UserError(_,p) ->
errorlabstrm "_" (str "on expr : " ++ Printer.pr_lconstr e ++ str " " ++ p)
-(* ['a info] contains the local information for travelling *)
+(* ['a info] contains the local information for traveling *)
type 'a infos =
{ nb_arg : int; (* function number of arguments *)
concl_tac : tactic; (* final tactic to finish proofs *)
@@ -337,7 +337,7 @@ type 'a infos =
f_id : Id.t; (* function name *)
f_constr : constr; (* function term *)
f_terminate : constr; (* termination proof term *)
- func : global_reference; (* functionnal reference *)
+ func : global_reference; (* functional reference *)
info : 'a;
is_main_branch : bool; (* on the main branch or on a matched expression *)
is_final : bool; (* final first order term or not *)
@@ -357,7 +357,7 @@ type ('a,'b) journey_info_tac =
'b infos -> (* argument of the tactic *)
tactic
-(* journey_info : specifies the actions to do on the different term constructors during the travelling of the term
+(* journey_info : specifies the actions to do on the different term constructors during the traveling of the term
*)
type journey_info =
{ letiN : ((Name.t*constr*types*constr),constr) journey_info_tac;
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-27 07:52:13 +0000