diff options
| author | herbelin | 2008-02-06 18:23:36 +0000 |
|---|---|---|
| committer | herbelin | 2008-02-06 18:23:36 +0000 |
| commit | 30c687b1fd0d2d9d3299f71971dc230cdd042e79 (patch) | |
| tree | 8830e3f5198f2a555523a70f5d136990fffdb216 /library | |
| parent | 4b935f808bc7f6b29c6e272b73a8af0e4738e303 (diff) | |
- 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
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |