diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/fourier/fourierR.ml | 3 | ||||
| -rw-r--r-- | contrib/ring/quote.ml | 7 |
2 files changed, 6 insertions, 4 deletions
diff --git a/contrib/fourier/fourierR.ml b/contrib/fourier/fourierR.ml index d415cf7d24..ef0ff426dc 100644 --- a/contrib/fourier/fourierR.ml +++ b/contrib/fourier/fourierR.ml @@ -503,8 +503,7 @@ let rec fourier gl= let res=fourier_lineq (!lineq) in let tac=ref tclIDTAC in if res=[] - then (print_string "Tactic Fourier fails.\n"; - flush stdout) + then Util.error "fourier failed" (* l'algorithme de Fourier a réussi: on va en tirer une preuve Coq *) else (match res with [(cres,sres,lc)]-> diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 3c1645d477..3b13283e13 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -191,8 +191,11 @@ let decomp_term c = kind_of_term (strip_outer_cast c) ?2 ?1)}, where \texttt{C} is the [i]-th constructor of inductive type [typ] *) -let coerce_meta_out id = int_of_string (string_of_id id) -let coerce_meta_in n = id_of_string (string_of_int n) +let coerce_meta_out id = + let s = string_of_id id in + int_of_string (String.sub s 1 (String.length s - 1)) +let coerce_meta_in n = + id_of_string ("M" ^ string_of_int n) let compute_lhs typ i nargsi = match kind_of_term typ with |