From: acondolu <andrea.condoluci@unibo.it>
Date: Sat, 22 Jul 2017 19:58:31 +0000 (+0200)
Subject: Renamed in critical_showstoppers: showstoppers -> inedible (I don't know why)
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=dc829653c03f7bf0977addabe480e7c8b178bad1;p=fireball-separation.git

Renamed in critical_showstoppers: showstoppers -> inedible (I don't know why)
---

diff --git a/ocaml/lambda4.ml b/ocaml/lambda4.ml
index dfe0da1..392784f 100644
--- a/ocaml/lambda4.ml
+++ b/ocaml/lambda4.ml
@@ -436,11 +436,11 @@ let eat p =
   let showstoppers = showstoppers_step @ showstoppers_eat in
   let heads = List.sort compare (filter_map hd_of ps) in
   let arities = precompute_edible_data p (uniq heads) in
-  let showstoppers, showstoppers_conv = edible p arities showstoppers in
-  let l = List.filter (fun (_,hd,_) -> not (List.mem hd showstoppers)) arities in
+  let inedible, showstoppers_conv = edible p arities showstoppers in
+  let l = List.filter (fun (_,hd,_) -> not (List.mem hd inedible)) arities in
   let p =
   List.fold_left (fun p (pos,hd,nargs) -> if pos = -1 then p else
-   let v = `N(pos) in
+   let v = `N pos in
    let inst = make_lams v nargs in
 prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ string_of_term p inst);
    { p with sigma = p.sigma @ [hd,inst] }
@@ -457,7 +457,7 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
  let p = match p.div with
   | None -> p
   | Some div ->
-   if List.mem (hd_of_i_var div) showstoppers
+   if List.mem (hd_of_i_var div) inedible
    then p
    else
     let n = match div with `I(_,args) -> Listx.length args | `Var _ -> 0 in
@@ -465,14 +465,14 @@ prerr_endline ("# INST_IN_EAT: " ^ string_of_var p.var_names hd ^ " := " ^ strin
     let inst = make_lams `Bottom n in
     subst_in_problem x inst p in
  let dangerous_conv = showstoppers_conv in
-let _ = prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
-List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv; in
+prerr_endline ("dangerous_conv lenght:" ^ string_of_int (List.length dangerous_conv));
+List.iter (fun l -> prerr_endline (String.concat " " (List.map (string_of_var p.var_names) l))) dangerous_conv;
  let conv =
    List.map (function s,t ->
     try
      if s <> [] then t else (
      (match t with | `Var _ -> raise Not_found | _ -> ());
-     let _ = List.find (fun h -> hd_of t = Some h) showstoppers in
+     let _ = List.find (fun h -> hd_of t = Some h) inedible in
       t)
     with Not_found -> match hd_of t with
      | None -> assert (t = convergent_dummy); t