From 6687f07e8e5e4d61034f9e7d61284be571bc528d Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 27 Jul 2010 13:49:31 +0000 Subject: 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 --- toplevel/command.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) 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 -- cgit v1.2.3