From 30c687b1fd0d2d9d3299f71971dc230cdd042e79 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 6 Feb 2008 18:23:36 +0000
Subject: - Documentation des nouvelles options d'implicites (Set Strongly
 Strict   Implicit, Set Maximal Implicit Insertion, Set Reversible Pattern  
 Implicit, Set Printing Implicit Defensive). - Changement de la sémantique de
 Set Strongly Strict Implicit : il   contient maintenant Set Strict Implicit.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10520 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 687374c59e..081bb58c10 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -237,7 +237,8 @@ let rec prepare_implicits f = function
 
 let compute_implicits_flags env f all t = 
   compute_implicits_gen 
-    f.strict f.strongly_strict f.reversible_pattern f.contextual all env t
+    (f.strict or f.strongly_strict) f.strongly_strict
+    f.reversible_pattern f.contextual all env t
     
 let compute_implicits_auto env f t =
   let l = compute_implicits_flags env f false t in
-- 
cgit v1.2.3