diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-10 12:45:54 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-09-10 12:45:54 +0000 |
| commit | 6f764a0a46cdeedc43be1349f5cd06d569bc45a0 (patch) | |
| tree | ee74bbeac061dcada38c37e80eae2091dd6804b9 /contrib | |
| parent | 055887ac67ed8bb7917408e23b1496f094d97ccd (diff) | |
profondeur maximale
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11395 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/dp/dp_gappa.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/dp/dp_gappa.ml b/contrib/dp/dp_gappa.ml index 70439a970..f77f1a5c4 100644 --- a/contrib/dp/dp_gappa.ml +++ b/contrib/dp/dp_gappa.ml @@ -160,7 +160,7 @@ let call_gappa hl p = let c = open_out gappa_out3 in let gappa2 = Filename.chop_suffix (Filename.basename gappa_out2) ".v" in Printf.fprintf c - "Require \"%s\". Set Printing Depth 9999999. Print %s.proof." + "Require \"%s\". Set Printing Depth 999999. Print %s.proof." (Filename.chop_suffix gappa_out2 ".v") gappa2; close_out c; let lambda = temp_file "gappa_lambda" in |