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 /interp/constrextern.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 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index ff494c782..0fe01799e 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -719,7 +719,8 @@ let rec extern inctx scopes vars r = let (ids,bl) = extern_local_binder scopes vars bl 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,nv.(i), bl, extern_typ scopes vars0 ty, + let n, ro = fst nv.(i), extern_recursion_order scopes vars (snd nv.(i)) in + (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) @@ -834,6 +835,11 @@ and extern_symbol (tmp_scope,scopes as allscopes) vars t = function with No_match -> extern_symbol allscopes vars t rules +and extern_recursion_order scopes vars = function + RStructRec -> CStructRec + | RWfRec c -> CWfRec (extern true scopes vars c) + + let extern_rawconstr vars c = extern false (None,Notation.current_scopes()) vars c |