diff options
author | 2007-04-29 11:38:19 +0000 | |
---|---|---|
committer | 2007-04-29 11:38:19 +0000 | |
commit | 10648acd7c8c4db1de25c785db4d192eaf2638e6 (patch) | |
tree | bf8ee6604092f6f3586bc95c62eb2f02521781fd /interp/constrintern.ml | |
parent | ac8b30a9d072b7f4b6803ec7283d2661f0d45505 (diff) |
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
Diffstat (limited to 'interp/constrintern.ml')
-rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 77e6ba42c..9b3268930 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -44,6 +44,8 @@ let for_grammar f x = let variables_bind = ref false +let insert_maximal_implicit = ref false + (**********************************************************************) (* Internalisation errors *) @@ -1033,7 +1035,7 @@ let internalise sigma globalenv env allow_patvar lvar c = let eargs' = List.remove_assoc id eargs in intern enva a :: aux (n+1) impl' subscopes' eargs' rargs with Not_found -> - if rargs=[] & eargs=[] & + if rargs=[] & eargs=[] & not !insert_maximal_implicit & not (List.for_all is_status_implicit impl') then (* Less regular arguments than expected: don't complete *) (* with implicit arguments *) |