From 21aca613bc898b501b132e4f455e8aa6c89729ef Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 22 Dec 2005 08:32:31 +0000
Subject: Correction bugs commit précédent

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7695 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 6eacde19ad..0795009b66 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1070,7 +1070,7 @@ let intern_gen isarity sigma env
   internalise sigma (extract_ids env, tmp_scope,[])
     allow_soapp (ltacvars,Environ.named_context env, [], impls) c
 
-let intern_constr sigma env c = intern_gen true sigma env c 
+let intern_constr sigma env c = intern_gen false sigma env c 
 
 let intern_ltac isarity ltacvars sigma env c =
   intern_gen isarity sigma env ~ltacvars:ltacvars c
@@ -1102,7 +1102,7 @@ let interp_constr_judgment sigma env c =
 type ltac_sign = identifier list * unbound_ltac_var_map
 
 let interp_constrpattern sigma env c =
-  pattern_of_rawconstr (intern_constr sigma env c)
+  pattern_of_rawconstr (intern_gen false sigma env ~allow_soapp:true c)
 
 let interp_aconstr impls vars a =
   let env = Global.env () in
-- 
cgit v1.2.3