diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-07 14:00:31 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-02-07 14:00:31 +0000 |
| commit | a4e65b24e64dcec8f5cf605464d3bac148600234 (patch) | |
| tree | 3ec447d6532c5ee43b0de279b6ef6052eb69cf57 /interp | |
| parent | 87fe3328d4f6230b10cf54a15f5ff1c073931e03 (diff) | |
Bug affichage rawconstr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6696 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrextern.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 46505450f..a5b022058 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1605,13 +1605,15 @@ let rec extern inctx scopes vars r = | RLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,nal, - (Some na,option_app (extern_typ scopes (add_vname vars na)) typopt), + (option_app (fun _ -> na) typopt, + option_app (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars tm, extern false scopes (List.fold_left add_vname vars nal) b) | RIf (loc,c,(na,typopt),b1,b2) -> CIf (loc,sub_extern false scopes vars c, - (Some na,option_app (extern_typ scopes (add_vname vars na)) typopt), + (option_app (fun _ -> na) typopt, + option_app (extern_typ scopes (add_vname vars na)) typopt), sub_extern false scopes vars b1, sub_extern false scopes vars b2) | RRec (loc,fk,idv,blv,tyv,bv) -> |