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/recdef | |
| 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/recdef')
| -rw-r--r-- | contrib/recdef/recdef.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
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 |