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 --- parsing/g_constr.ml4 | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'parsing/g_constr.ml4') diff --git a/parsing/g_constr.ml4 b/parsing/g_constr.ml4 index 3b32cfd47..6b6b4871c 100644 --- a/parsing/g_constr.ml4 +++ b/parsing/g_constr.ml4 @@ -55,7 +55,7 @@ let mk_fixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty | None -> CHole (loc, None) in - (snd id,(n,ro),bl,ty,body) + (id,(n,ro),bl,ty,body) let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let _ = Option.map (fun (aloc,_) -> @@ -65,7 +65,7 @@ let mk_cofixb (id,bl,ann,body,(loc,tyc)) = let ty = match tyc with Some ty -> ty | None -> CHole (loc, None) in - (snd id,bl,ty,body) + (id,bl,ty,body) let mk_fix(loc,kw,id,dcls) = if kw then -- cgit v1.2.3