fixed bug in coercion application, input/output swapped in unification

[helm.git] / helm / software / components / acic_procedural / proceduralTypes.ml

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index c465315d4bc183b1e1a7c1ef8f852bff310dd829..45fbe756aa2da62ec4c39d435f346e89bec51de0 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -174,7 +174,7 @@ let mk_record types lpsno fields =
 
 let mk_statement flavour name t v =
    let name = match name with Some name -> name | None -> assert false in
-   let obj = N.Theorem (flavour, name, t, v) in
+   let obj = N.Theorem (flavour, name, t, v, `Regular) in
    G.Executable (floc, G.Command (floc, G.Obj (floc, obj)))
 
 let mk_qed =