diff options
Diffstat (limited to 'plugins/cc')
| -rw-r--r-- | plugins/cc/ccalgo.ml | 4 | ||||
| -rw-r--r-- | plugins/cc/cctac.ml | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml index 26fd43a68e..0970717edd 100644 --- a/plugins/cc/ccalgo.ml +++ b/plugins/cc/ccalgo.ml @@ -68,7 +68,7 @@ module ST=struct with Not_found -> () - let rec delete_set st s = Intset.iter (delete st) s + let delete_set st s = Intset.iter (delete st) s end @@ -781,7 +781,7 @@ let make_fun_table state = !funtab -let rec do_match state res pb_stack = +let do_match state res pb_stack = let mp=Stack.pop pb_stack in match mp.mp_stack with [] -> diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml index 07813741c7..2042f9b058 100644 --- a/plugins/cc/cctac.ml +++ b/plugins/cc/cctac.ml @@ -179,7 +179,7 @@ let litteral_of_constr env sigma term= (* store all equalities from the context *) -let rec make_prb gls depth additionnal_terms = +let make_prb gls depth additionnal_terms = let env=pf_env gls in let sigma=sig_sig gls in let state = empty depth gls in |