Imported Upstream version 8.0pl3+8.1betaupstream/8.0pl3+8.1beta

1 files changed, 0 insertions, 34 deletions

diff --git a/contrib/funind/new_arg_principle.mli b/contrib/funind/new_arg_principle.mli
deleted file mode 100644
index cad68da6..00000000
--- a/contrib/funind/new_arg_principle.mli
+++ /dev/null
@@ -1,34 +0,0 @@
-
-val generate_functional_principle : 
-  (* do we accept interactive proving *)
-  bool ->
-  (* induction principle on rel *) 
-  Term.types ->
-  (* *)
-  Term.sorts array option -> 
-  (* Name of the new principle *) 
-  (Names.identifier) option -> 
-  (* the compute functions to use   *)
-  Names.constant array -> 
-  (* We prove the nth- principle *)
-  int  ->
-  (* The tactic to use to make the proof w.r
-     the number of params
-  *)
-  (Term.constr array -> int -> Tacmach.tactic) -> 
-  unit
-
-
-
-(* val my_reflexivity : Tacmach.tactic  *)
-
-val prove_princ_for_struct : 
-  bool -> 
-  int -> Names.constant array -> Term.constr array -> int -> Tacmach.tactic
-
-
-val compute_new_princ_type_from_rel : Term.constr array -> Term.sorts array -> 
-  Term.types -> Term.types
-
-val make_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort) list ->  unit
-val make_case_scheme : (Names.identifier*Names.identifier*Rawterm.rawsort)  ->  unit