diff options
| author | msozeau | 2008-05-30 12:41:39 +0000 |
|---|---|---|
| committer | msozeau | 2008-05-30 12:41:39 +0000 |
| commit | f350cd8cb53e675a5793336b9b17c4749fa474b8 (patch) | |
| tree | f39b9330fe34e7447dbbc09121b16cb97330cdd7 /interp/constrextern.ml | |
| parent | 3ed23b97c8d1bfbf917b540a35ee767afea28658 (diff) | |
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
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index dedaf6af4a..c922503aab 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -726,7 +726,7 @@ let rec extern inctx scopes vars r = | Some x -> Some (dummy_loc, out_name (List.nth ids x)) in let ro = extern_recursion_order scopes vars (snd nv.(i)) in - (fi, (n, ro), bl, extern_typ scopes vars0 ty, + ((dummy_loc, fi), (n, ro), bl, extern_typ scopes vars0 ty, extern false scopes vars1 def)) idv in CFix (loc,(loc,idv.(n)),Array.to_list listdecl) @@ -736,7 +736,7 @@ let rec extern inctx scopes vars r = let (ids,bl) = extern_local_binder scopes vars blv.(i) in let vars0 = List.fold_right (name_fold Idset.add) ids vars in let vars1 = List.fold_right (name_fold Idset.add) ids vars' in - (fi,bl,extern_typ scopes vars0 tyv.(i), + ((dummy_loc, fi),bl,extern_typ scopes vars0 tyv.(i), sub_extern false scopes vars1 bv.(i))) idv in CCoFix (loc,(loc,idv.(n)),Array.to_list listdecl)) |