diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 11:41:58 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-04-28 11:41:58 +0000 |
| commit | f3e237894067f3d3548d6cba5a64c2b8193a88d3 (patch) | |
| tree | a53be7ef3cb3dfccabade87c53889faaa6dd5535 /pretyping/rawterm.mli | |
| parent | eb6d5b6acaca83d13063f0d7fc414b4dbee6572e (diff) | |
Changement de représentation du contexte des réf dans rawconstr et pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@377 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/rawterm.mli')
| -rw-r--r-- | pretyping/rawterm.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli index f78520a16..5f67a8a92 100644 --- a/pretyping/rawterm.mli +++ b/pretyping/rawterm.mli @@ -32,7 +32,7 @@ type 'ctxt reference = | RMeta of int type rawconstr = - | RRef of loc * rawconstr array reference + | RRef of loc * Term.constr array reference | RApp of loc * rawconstr * rawconstr list | RBinder of loc * binder_kind * name * rawconstr * rawconstr | RCases of loc * Term.case_style * rawconstr option * rawconstr list * @@ -61,7 +61,7 @@ val dummy_loc : loc val loc_of_rawconstr : rawconstr -> loc type constr_pattern = - | PRef of constr_pattern array reference + | PRef of Term.constr array reference | PRel of int | PApp of constr_pattern * constr_pattern array | PSoApp of int * int list |