diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-26 13:51:24 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-12-26 13:51:24 +0000 |
| commit | e0f9487be5ce770117a9c9c815af8c7010ff357b (patch) | |
| tree | bbbde42b0a40803a0c5f5bdb5aaf09248d9aedc0 /interp/reserve.ml | |
| parent | 98d60ce261e7252379ced07d2934647c77efebfd (diff) | |
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanismes de renommage des noms de constantes, de module, de ltac et de certaines variables liées de lemmes et de tactiques, mécanisme d'ajout d'arguments implicites, etc.)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7732 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/reserve.ml')
| -rw-r--r-- | interp/reserve.ml | 8 |
1 files changed, 2 insertions, 6 deletions
diff --git a/interp/reserve.ml b/interp/reserve.ml index 917f9f4ad..834587f8d 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -57,14 +57,11 @@ let rec unloc = function | RLambda (_,na,ty,c) -> RLambda (dummy_loc,na,unloc ty,unloc c) | RProd (_,na,ty,c) -> RProd (dummy_loc,na,unloc ty,unloc c) | RLetIn (_,na,b,c) -> RLetIn (dummy_loc,na,unloc b,unloc c) - | RCases (_,(tyopt,rtntypopt),tml,pl) -> + | RCases (_,rtntypopt,tml,pl) -> RCases (dummy_loc, - (option_app unloc tyopt,ref (option_app unloc !rtntypopt)), + (option_app unloc rtntypopt), List.map (fun (tm,x) -> (unloc tm,x)) tml, List.map (fun (_,idl,p,c) -> (dummy_loc,idl,p,unloc c)) pl) - | ROrderedCase (_,b,tyopt,tm,bv,x) -> - ROrderedCase - (dummy_loc,b,option_app unloc tyopt,unloc tm, Array.map unloc bv,x) | RLetTuple (_,nal,(na,po),b,c) -> RLetTuple (dummy_loc,nal,(na,option_app unloc po),unloc b,unloc c) | RIf (_,c,(na,po),b1,b2) -> @@ -86,7 +83,6 @@ let rec unloc = function let anonymize_if_reserved na t = match na with | Name id as na -> - if !Options.v7 & id = id_of_string "_" then t else (try if unloc t = find_reserved_type id then RHole (dummy_loc,Evd.BinderType na) |