Une MAJ de sécurité est nécessaire sur notre version actuelle. Elle sera effectuée lundi 02/08 entre 12h30 et 13h. L'interruption de service devrait durer quelques minutes (probablement moins de 5 minutes).

Commit a98734ca authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

do not produce triggers for definitions (they are either trivial or wrong)

parent 63047339
......@@ -86,13 +86,13 @@ let add_ld func pred axl d = match d with
| Term t when func ->
let nm = ls.ls_name.id_string ^ "_def" in
let hd = t_app ls (List.map t_var vl) t.t_ty in
let ax = f_forall_close vl [[Term hd]] (t_insert hd t) in
let ax = f_forall_close vl [] (t_insert hd t) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr ax :: axl, (ls, None)
| Fmla f when pred ->
let nm = ls.ls_name.id_string ^ "_def" in
let hd = f_app ls (List.map t_var vl) in
let ax = f_forall_close vl [[Fmla hd]] (f_insert hd f) in
let ax = f_forall_close vl [] (f_insert hd f) in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
create_prop_decl Paxiom pr ax :: axl, (ls, None)
| _ -> axl, d
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment