diff options
| author | herbelin | 2000-03-21 00:03:37 +0000 |
|---|---|---|
| committer | herbelin | 2000-03-21 00:03:37 +0000 |
| commit | 73e027a781c1025914749975d341dbab21e2bc45 (patch) | |
| tree | 588e9ef6035cd7d48346e9dba7ab15c1e4490fef /pretyping | |
| parent | 1c1b6f2da919c1303b87b97119b621a06952fadc (diff) | |
Prise en compte nouveau case_info
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@334 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/rawterm.ml | 4 | ||||
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
2 files changed, 2 insertions, 6 deletions
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml index c3f7d8822c..ec43265658 100644 --- a/pretyping/rawterm.ml +++ b/pretyping/rawterm.ml @@ -30,13 +30,11 @@ type reference = | REVar of int * identifier list | RMeta of int -type cases_style = PrintLet | PrintIf | PrintCases - type rawconstr = | RRef of loc * reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr - | RCases of loc * cases_style * rawconstr option * rawconstr list * + | RCases of loc * Term.case_style * rawconstr option * rawconstr list * (identifier list * pattern list * rawconstr) list | ROldCase of loc * bool * rawconstr option * rawconstr * rawconstr array diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index 8c93eecd9f..c31691046d 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -30,13 +30,11 @@ type reference = | REVar of int * identifier list | RMeta of int -type cases_style = PrintLet | PrintIf | PrintCases - type rawconstr = | RRef of loc * reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr - | RCases of loc * cases_style * rawconstr option * rawconstr list * + | RCases of loc * Term.case_style * rawconstr option * rawconstr list * (identifier list * pattern list * rawconstr) list | ROldCase of loc * bool * rawconstr option * rawconstr * rawconstr array |