diff options
Diffstat (limited to 'contrib/interface')
| -rwxr-xr-x | contrib/interface/blast.ml | 2 | ||||
| -rw-r--r-- | contrib/interface/showproof.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/contrib/interface/blast.ml b/contrib/interface/blast.ml index a7e98b69dc..d5236a7a9f 100755 --- a/contrib/interface/blast.ml +++ b/contrib/interface/blast.ml @@ -506,7 +506,7 @@ let full_auto n gl = tclTRY (search n db_list (make_local_hint_db gl) hyps) gl let default_full_auto gl = full_auto !default_search_depth gl -(***********************************************************************) +(************************************************************************) let blast_tactic = ref (free_try default_full_auto) ;; diff --git a/contrib/interface/showproof.ml b/contrib/interface/showproof.ml index 5918a8b7ee..5b265ec864 100644 --- a/contrib/interface/showproof.ml +++ b/contrib/interface/showproof.ml @@ -1676,7 +1676,7 @@ and natural_induction ig lh g gs ge arg2 ltree with_intros= ]) ltree)) ] -(***********************************************************************) +(************************************************************************) (* Points fixes *) and natural_fix ig lh g gs narg ltree = |