diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 08:35:21 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 08:35:21 +0000 |
| commit | c300bc395fb987f7ded64c17bce5c966c0279442 (patch) | |
| tree | 443364b05d14feb412ba7a1a66ebc6ee1b6d8b2e /pretyping | |
| parent | 1fda9cc1a2d8c2db92d88d3e2715d3ee86f90bf3 (diff) | |
- coqc : option -image
- coqmktop : manquaient des -I
- tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau
- correction d'un bug de Simpl avec Fix (découvert dans preuve FTA)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/tacred.ml | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 0c5dc14e0..9b78d19a9 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -88,7 +88,12 @@ let check_fix_reversibility labs args ((lv,i),(tys,_,bds)) = raise Elimconst) args in if list_distinct (List.map fst li) then - EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n)) + let k = lv.(i) in + if k < nargs then + let p = destRel (List.nth args k) in + EliminationFix (n-p+1,(nbfix,li,n)) + else + EliminationFix (n-nargs+lv.(i)+1,(nbfix,li,n)) else raise Elimconst |