diff options
| author | msozeau | 2006-03-13 17:38:17 +0000 |
|---|---|---|
| committer | msozeau | 2006-03-13 17:38:17 +0000 |
| commit | db6c97df4dde8b1ccb2e5b314a4747f66fd524c1 (patch) | |
| tree | 39ba546322e7f3d4bd4cc9d58260d3f1b4114bd5 /pretyping/rawterm.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 'pretyping/rawterm.ml')
| -rw-r--r-- | pretyping/rawterm.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index d06395b09d..1c59004175 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -34,8 +34,6 @@ type patvar = identifier type rawsort = RProp of Term.contents | RType of Univ.universe option -type fix_kind = RFix of (int array * int) | RCoFix of int - type binder_kind = BProd | BLambda | BLetIn type quantified_hypothesis = AnonHyp of int | NamedHyp of identifier @@ -73,6 +71,10 @@ type rawconstr = and rawdecl = name * rawconstr option * rawconstr +and fix_recursion_order = RStructRec | RWfRec of rawconstr + +and fix_kind = RFix of ((int * fix_recursion_order) array * int) | RCoFix of int + let cases_predicate_names tml = List.flatten (List.map (function | (tm,(na,None)) -> [na] |