diff options
| author | herbelin | 2005-02-18 22:12:06 +0000 |
|---|---|---|
| committer | herbelin | 2005-02-18 22:12:06 +0000 |
| commit | afaf46e385a1a0f05e7605592831bde38b7dcc41 (patch) | |
| tree | a41d5622486c2966fb1c0fd5d13df5a71aa67f17 | |
| parent | 4bc680136b9310f7ab630e41b47314b9efdbe9d2 (diff) | |
Déboggueur et code mort
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6742 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | contrib/omega/coq_omega.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml index 41eec8dc85..aaabf65331 100644 --- a/contrib/omega/coq_omega.ml +++ b/contrib/omega/coq_omega.ml @@ -111,7 +111,7 @@ let new_var_num = let new_var = let cpt = ref 0 in fun () -> incr cpt; Nameops.make_ident "WW" (Some !cpt) -let display_var i = Printf.sprintf "O%d" i +let display_var i = Printf.sprintf "X%d" i let intern_id,unintern_id = let cpt = ref 0 in @@ -1208,7 +1208,6 @@ let replay_history tactic_normalisation = in let mm = mk_integer m in let p_initial = [P_APP 2;P_TYPE] in - let r = mk_plus eq2 (mk_times (mk_plus (mk_inv (mkVar vid)) eq1) mm) in let tac = clever_rewrite (P_APP 1 :: P_APP 1 :: P_APP 2 :: p_initial) [[P_APP 1]] (Lazy.force coq_fast_Zopp_one) :: |