diff options
| author | barras | 2004-02-18 18:32:33 +0000 |
|---|---|---|
| committer | barras | 2004-02-18 18:32:33 +0000 |
| commit | b5df1925bbc14f441247349b200aa3f5828e8427 (patch) | |
| tree | c158ac5d3d3133f2fce8188f3d0b4a75bd0c5415 /interp/constrextern.ml | |
| parent | 06900e469cd593c272f57c2af7d2e4f206a2f944 (diff) | |
- fixed the Assert_failure error in kernel/modops
- fixed the problem with passing atomic tactics to ltacs
- restructured the distrib Makefile (can build a package from
the CVS working dir)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'interp/constrextern.ml')
| -rw-r--r-- | interp/constrextern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 60e6657d54..e28065afd8 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1493,13 +1493,13 @@ let rec extern inctx scopes vars r = | RLetTuple (loc,nal,(na,typopt),tm,b) -> CLetTuple (loc,nal, - (na,option_app (extern_type scopes (add_vname vars na)) typopt), + (Some na,option_app (extern_type 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, - (na,option_app (extern_type scopes (add_vname vars na)) typopt), + (Some na,option_app (extern_type scopes (add_vname vars na)) typopt), sub_extern false scopes vars b1, sub_extern false scopes vars b2) | RRec (loc,fk,idv,tyv,bv) -> |