From 7a39bd5650cc49c5c77788fb42fe2caaf35dfdac Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 6 May 2008 14:05:20 +0000 Subject: Postpone the search for the recursive argument index from the user given name after internalisation, to get the correct behavior with typeclass binders. This simplifies the pretty printing and translation of the recursive argument name in various places too. Use this opportunity to factorize the different internalization and interpretation functions of binders as well. This definitely fixes part 2 of bug #1846 and makes it possible to use fixpoint definitions with typeclass arguments in program too, with an example given in EquivDec. At the same time, one fix and one enhancement in Program: - fix a de Bruijn bug in subtac_cases - introduce locations of obligations and use them in case the obligation tactic raises a failure when tried on a particular obligation, as suggested by Sean Wilson. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10889 85f007b7-540e-0410-9357-904b9bb8a0f7 --- toplevel/record.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'toplevel/record.ml') diff --git a/toplevel/record.ml b/toplevel/record.ml index 57a7e63b3..f6815d537 100644 --- a/toplevel/record.ml +++ b/toplevel/record.ml @@ -43,7 +43,7 @@ let interp_decl sigma env = function let typecheck_params_and_fields id t ps fs = let env0 = Global.env () in - let env1,newps = interp_context Evd.empty env0 ps in + let (env1,newps), _ = interp_context Evd.empty env0 ps in let fullarity = it_mkProd_or_LetIn t newps in let env_ar = push_rel_context newps (push_rel (Name id,None,fullarity) env0) in let env2,newfs = -- cgit v1.2.3