From b5df1925bbc14f441247349b200aa3f5828e8427 Mon Sep 17 00:00:00 2001
From: barras
Date: Wed, 18 Feb 2004 18:32:33 +0000
Subject: - 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
---
 interp/constrextern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp/constrextern.ml')

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) ->
-- 
cgit v1.2.3