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/detyping.ml | |
| 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/detyping.ml')
| -rw-r--r-- | pretyping/detyping.ml | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml index 2dd49e4b7..a7c84dd3c 100644 --- a/pretyping/detyping.ml +++ b/pretyping/detyping.ml @@ -315,17 +315,13 @@ let rec detype avoid env t = | IsAppL (f,args) -> RApp (dummy_loc,detype avoid env f,List.map (detype avoid env) args) | IsConst (sp,cl) -> - RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl)) + RRef(dummy_loc,RConst(sp,cl)) | IsEvar (ev,cl) -> - RRef(dummy_loc,REVar(ev,Array.map (detype avoid env) cl)) + RRef(dummy_loc,REVar(ev,cl)) | IsAbst (sp,cl) -> anomaly "bdize: Abst should no longer occur in constr" - | IsMutInd (ind_sp,cl) -> - let ctxt = Array.map (detype avoid env) cl in - RRef (dummy_loc,RInd (ind_sp,ctxt)) - | IsMutConstruct (cstr_sp,cl) -> - let ctxt = Array.map (detype avoid env) cl in - RRef (dummy_loc,RConstruct (cstr_sp,ctxt)) + | IsMutInd (ind_sp,cl) -> RRef (dummy_loc,RInd (ind_sp,cl)) + | IsMutConstruct (cstr_sp,cl) -> RRef (dummy_loc,RConstruct (cstr_sp,cl)) | IsMutCase (annot,p,c,bl) -> let synth_type = synthetize_type () in let tomatch = detype avoid env c in |