diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-27 13:49:31 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-07-27 13:49:31 +0000 |
| commit | 6687f07e8e5e4d61034f9e7d61284be571bc528d (patch) | |
| tree | 398113ae7dddd2e9d6c06bcb792acda79e5b970c /toplevel | |
| parent | a73354053c8e6e9c1d02320f622fe8408526b5e6 (diff) | |
Fix computation of fix annotation index: only consider assumptions and
not let-ins in the binding list.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13335 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/command.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index b60cbe9cd..3f4f15318 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -455,7 +455,8 @@ let interp_fix_context evdref env isfix fix = let before, after = if isfix then split_at_annot fix.fix_binders fix.fix_annot else [], fix.fix_binders in let (env', ctx), imps = interp_context_evars evdref env before in let (env'', ctx'), imps' = interp_context_evars evdref env' after in - ((env'', ctx' @ ctx), imps @ imps', Option.map (fun _ -> List.length ctx) fix.fix_annot) + let annot = Option.map (fun _ -> List.length (assums_of_rel_context ctx)) fix.fix_annot in + ((env'', ctx' @ ctx), imps @ imps', annot) let interp_fix_ccl evdref (env,_) fix = interp_type_evars evdref env fix.fix_type |