diff options
| author |  courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 12:52:38 +0000 |
|---|---|---|
| committer | courtieu <courtieu@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2003-03-31 12:52:38 +0000 |
| commit | 8a8b61d623dd1a37cf5a7edb4d77ba8cae893085 (patch) | |
| tree | 7cce7e4d048ea48bc2ba408a14c3e25ddbdf6cab /contrib/funind/tacinvutils.mli | |
| parent | f5bdbc026f6aa9456aa3850451942f72f9c9190e (diff) | |
Correcting a bug occuring when the mimicked function had a
lambda-abstraction inside a Cases. I had to make the term of the
induction principle a bit less clean (more eta expansions).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3817 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/funind/tacinvutils.mli')
| -rw-r--r-- | contrib/funind/tacinvutils.mli | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/contrib/funind/tacinvutils.mli b/contrib/funind/tacinvutils.mli index 21e351371..b42182890 100644 --- a/contrib/funind/tacinvutils.mli +++ b/contrib/funind/tacinvutils.mli @@ -21,7 +21,7 @@ open Refine open Evd (*i*) -(* printing *) +(* printing debugging *) val prconstr: constr -> unit val prlistconstr: constr list -> unit val prstr: string -> unit @@ -29,6 +29,8 @@ val prstr: string -> unit val mknewmeta: unit -> constr val mknewexist: unit -> existential +val resetmeta: unit -> unit (* safe *) +val resetexist: unit -> unit (* be careful with this one *) val mkevarmap_from_listex: (Term.existential * Term.types) list -> evar_map val mkEq: types -> constr -> constr -> constr (* let mkEq typ c1 c2 = mkApp (build_coq_eq_data.eq(),[| typ; c1; c2|]) *) @@ -50,12 +52,12 @@ val prod_id: constr -> constr -> constr -> constr val name_of_string : string -> name val newname_append: name -> string -> name -val apply_eqtrpl: (constr*constr*constr) -> constr -> constr +val apply_eqtrpl: constr*(constr*constr*constr) -> constr -> constr val substitterm: int -> constr -> constr -> constr -> constr val apply_leqtrpl_t: - constr -> (constr*constr*constr) list -> constr + constr -> (constr*(constr*constr*constr)) list -> constr val apply_eq_leqtrpl: - (constr*constr*constr) list -> constr -> (constr*constr*constr) list + (constr*(constr*constr*constr)) list -> constr -> (constr*(constr*constr*constr)) list (* val apply_leq_lt: constr list -> constr list -> constr list *) val hdMatchSub: constr -> constr -> constr list |