From f350cd8cb53e675a5793336b9b17c4749fa474b8 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 30 May 2008 12:41:39 +0000
Subject: Improvements on coqdoc by adding more information into .glob files,
 about definitions and type of references. - Add missing location information
 on fixpoints/cofixpoint in topconstr and syntactic definitions in
 vernacentries for correct dumping. - Dump definition information in
 vernacentries: defs, constructors, projections etc... - Modify
 coqdoc/index.mll to use this information instead of trying to scan the file.
 - Use the type information in latex output, update coqdoc.sty accordingly. -
 Use the hyperref package to do crossrefs between definition and   references
 to coq objects in latex.

Next step is to test and debug it on bigger developments.

On the side:
- Fix Program Let which was adding a Global definition. 
- Correct implicits for well-founded Program Fixpoints.
- Add new [Method] declaration kind.


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11024 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/class_tactics.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics')

diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 5bd8f9f6fc..38fd3ab63f 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -434,7 +434,7 @@ END
 
 (** Typeclass-based rewriting. *)
 
-let respect_proj = lazy (mkConst (List.hd (Lazy.force morphism_class).cl_projs))
+let respect_proj = lazy (mkConst (snd (List.hd (Lazy.force morphism_class).cl_projs)))
 
 let make_dir l = make_dirpath (List.map id_of_string (List.rev l))
 
-- 
cgit v1.2.3