diff options
| author | courtieu | 2006-03-12 14:10:20 +0000 |
|---|---|---|
| committer | courtieu | 2006-03-12 14:10:20 +0000 |
| commit | d9cc734c4cd2a75a303cc08c3df0973077099ab1 (patch) | |
| tree | f87b19128dbb947ce70b47019234ac6dbb39ec91 /contrib | |
| parent | 071daf340720801328f0d79f1ef3f5b8a3a01415 (diff) | |
-Debugging multiple induction, a bug appeared when having function
arguments to a principle (like in map_ind).
-Added nbranches and npredicates to elim_scheme, and made the elimc
field optional.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8622 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/funind/indfun_main.ml4 | 2 | ||||
| -rw-r--r-- | contrib/funind/invfun.ml | 2 | ||||
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/contrib/funind/indfun_main.ml4 b/contrib/funind/indfun_main.ml4 index e7751c1649..f182c79978 100644 --- a/contrib/funind/indfun_main.ml4 +++ b/contrib/funind/indfun_main.ml4 @@ -74,7 +74,7 @@ TACTIC EXTEND newfunind ) with _ -> assert false) in - Tactics.compute_elim_sig (mkRel 0,Rawterm.NoBindings) princ_type + Tactics.compute_elim_sig princ_type in (* msg *) (* (str "computing non parameters argument for " ++ *) diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml index 767974c3ae..1f711297aa 100644 --- a/contrib/funind/invfun.ml +++ b/contrib/funind/invfun.ml @@ -107,7 +107,7 @@ let invfun (hypname:identifier) (fid:identifier) : tactic= ) with _ -> assert false) in - Tactics.compute_elim_sig (mkRel 0,Rawterm.NoBindings) princ_type + Tactics.compute_elim_sig princ_type in let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in let do_invert fargs appf : tactic = diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4 index 70c573220b..5bf0744d58 100644 --- a/contrib/recdef/recdef.ml4 +++ b/contrib/recdef/recdef.ml4 @@ -1265,7 +1265,7 @@ let prove_principle tcc_lemma_ref is_mes functional_ref fun g -> let type_of_goal = pf_concl g in let goal_ids = pf_ids_of_hyps g in - let goal_elim_infos = compute_elim_sig (mkRel 0,Rawterm.NoBindings) type_of_goal in + let goal_elim_infos = compute_elim_sig type_of_goal in let params_names,ids = List.fold_left (fun (params_names,avoid) (na,_,_) -> let new_id = fresh_id avoid na in |