From 10648acd7c8c4db1de25c785db4d192eaf2638e6 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 29 Apr 2007 11:38:19 +0000
Subject: Multiples changements autour des implicites :

- correction du mode strict qui n'était pas si strict,
- option "Set Strong Strict Implicit" pour activer le mode strictement
  strict (désactivé par défaut pour raison de compatibilité),
- option "Set Reversible Pattern Implicit" pour activer les implicites
  inférables par unification-pattern (désactivé par défaut par compatibilité),
- option "Unset Printing Implicit Defensive" pour désactiver
  l'affichage des implicites n'ayant pas été décelés stricts,
- option "Set Maximal Implicit Insertion" pour que les
  applications soient saturées en implicites si possible,
- une optimisation du mode non strict pour que l'algo de
  recherche des implicites renonce à calculer les occurrences non
  strictes qui pourraient avoir à être affichées dans le mode défensif,
  avec pour conséquence que le mode défensif, pour celui qui le veut,
  devient a priori encore plus verbeux, ex:

  Set Implicit Arguments.
  Definition id x : nat := x.
  Parameter f : forall n, id n = id n -> Prop.
  Check (f (refl_equal O)).
  (* Affichait: "f (refl_equal 0)" mais affiche maintenant 
     "f (n:=0) (refl_equal 0)" *)



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9812 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacentries.ml | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

(limited to 'toplevel')

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4c0fb5046f..b4777a43de 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -706,6 +706,14 @@ let _ =
       optread  = Impargs.is_strict_implicit_args;
       optwrite = Impargs.make_strict_implicit_args }
 
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "strong strict implicit arguments";
+      optkey   = (TertiaryTable ("Strong","Strict","Implicit"));
+      optread  = Impargs.is_strong_strict_implicit_args;
+      optwrite = Impargs.make_strong_strict_implicit_args }
+
 let _ =
   declare_bool_option 
     { optsync  = true;
@@ -714,6 +722,22 @@ let _ =
       optread  = Impargs.is_contextual_implicit_args;
       optwrite = Impargs.make_contextual_implicit_args }
 
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "implicit arguments defensive printing";
+      optkey   = (TertiaryTable ("Reversible","Pattern","Implicit"));
+      optread  = Impargs.is_reversible_pattern_implicit_args;
+      optwrite = Impargs.make_reversible_pattern_implicit_args }
+
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "maximal insertion of implicit";
+      optkey   = (TertiaryTable ("Maximal","Implicit","Insertion"));
+      optread  = (fun () -> !Constrintern.insert_maximal_implicit);
+      optwrite = (fun b ->  Constrintern.insert_maximal_implicit := b) }
+
 let _ =
   declare_bool_option 
     { optsync  = true;
@@ -730,6 +754,14 @@ let _ =
       optread  = (fun () -> !Constrextern.print_implicits);
       optwrite = (fun b ->  Constrextern.print_implicits := b) }
 
+let _ =
+  declare_bool_option 
+    { optsync  = true;
+      optname  = "implicit arguments defensive printing";
+      optkey   = (TertiaryTable ("Printing","Implicit","Defensive"));
+      optread  = (fun () -> !Constrextern.print_implicits_defensive);
+      optwrite = (fun b ->  Constrextern.print_implicits_defensive := b) }
+
 let _ =
   declare_bool_option 
     { optsync  = true;
-- 
cgit v1.2.3