diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-13 17:38:17 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-13 17:38:17 +0000 |
| commit | db6c97df4dde8b1ccb2e5b314a4747f66fd524c1 (patch) | |
| tree | 39ba546322e7f3d4bd4cc9d58260d3f1b4114bd5 /toplevel/command.ml | |
| parent | d9cc734c4cd2a75a303cc08c3df0973077099ab1 (diff) | |
Update of Subtac contrib. Add {wf n R} as an alternative to {struct n}.
May cause make world to fail because of dependency problems, make depend clean
world should fix that (hopefully).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8624 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel/command.ml')
| -rw-r--r-- | toplevel/command.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index 72139404b..9f8bbad25 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -501,7 +501,7 @@ let build_recursive (lnameargsardef:(fixpoint_expr *decl_notation) list) let recdecls = (Array.map (fun id -> Name id) namerec, arrec, recvec) in let rec declare i fi = let ce = - { const_entry_body = mkFix ((nvrec,i),recdecls); + { const_entry_body = mkFix ((Array.map fst nvrec,i),recdecls); (* ignore rec order *) const_entry_type = Some arrec.(i); const_entry_opaque = false; const_entry_boxed = boxed} in |