- Solved the Coq 8.5 problem relating to declaring section variables

- Correct equality check of atoms and formulas for processing congruence closure

3 files changed, 13 insertions, 13 deletions

diff --git a/src/verit/veritSyntax.ml b/src/verit/veritSyntax.ml
index c60d34f..3ff11e9 100644
--- a/src/verit/veritSyntax.ml
+++ b/src/verit/veritSyntax.ml
@@ -55,14 +55,14 @@ let is_eq l =
 
 let rec process_trans a b prem res =
   try
-    let (l,(c,c')) = List.find (fun (l,(a',b')) -> (a' = b || b' = b)) prem in
-    let prem = List.filter (fun l' -> l' <> (l,(c,c'))) prem in
-    let c = if c = b then c' else c in
-    if a = c
+    let (l,(c,c')) = List.find (fun (l,(a',b')) -> ((Atom.equal a' b) || (Atom.equal b' b))) prem in
+    let prem = List.filter (fun (l',(d,d')) -> (not (Form.equal l' l)) || (not (Atom.equal d c)) || (not (Atom.equal d' c'))) prem in
+    let c = if Atom.equal c b then c' else c in
+    if Atom.equal a c
     then List.rev (l::res)
     else process_trans a c prem (l::res)
   with
-    |Not_found -> if a = b then [] else assert false
+    |Not_found -> if Atom.equal a b then [] else assert false
 
 
 let mkTrans p =
@@ -84,7 +84,7 @@ let rec process_congr a_args b_args prem res =
       (* if a = b *)
       (* then process_congr a_args b_args prem (None::res) *)
       (* else *)
-        let (l,(a',b')) = List.find (fun (l,(a',b')) -> (a = a' && b = b')||(a = b' && b = a')) prem in
+        let (l,(a',b')) = List.find (fun (l,(a',b')) -> ((Atom.equal a a') && (Atom.equal b b'))||((Atom.equal a b') && (Atom.equal b a'))) prem in
         process_congr a_args b_args prem ((Some l)::res)
     | [],[] -> List.rev res
     | _ -> failwith "VeritSyntax.process_congr: incorrect number of arguments in function application"
@@ -108,7 +108,7 @@ let mkCongr p =
           let cert = process_congr a_args b_args prem_val [] in
           Other (EqCgr (c,cert))
         | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
-          if a_f = b_f then
+          if indexed_op_index a_f = indexed_op_index b_f then
             let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
             Other (EqCgr (c,cert))
           else failwith "VeritSyntax.mkCongr: left function is different from right fucntion"
@@ -131,7 +131,7 @@ let mkCongrPred p =
               let cert = process_congr a_args b_args prem_val [] in
               Other (EqCgrP (p_p,c,cert))
             | Aapp (a_f,a_args), Aapp (b_f,b_args) ->
-              if a_f = b_f then
+              if indexed_op_index a_f = indexed_op_index b_f then
                 let cert = process_congr (Array.to_list a_args) (Array.to_list b_args) prem_val [] in
                 Other (EqCgrP (p_p,c,cert))
               else failwith "VeritSyntax.mkCongrPred: unmatching predicates"
diff --git a/src/versions/standard/structures.ml b/src/versions/standard/structures.ml
index bd9e4f4..08451c9 100644
--- a/src/versions/standard/structures.ml
+++ b/src/versions/standard/structures.ml
@@ -85,11 +85,11 @@ let error = Errors.error
 let coqtype = Future.from_val Term.mkSet
 
 let declare_new_type t =
-  let _ = Command.declare_assumption false (Decl_kinds.Local, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, t) in
+  let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (Future.force coqtype, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, t) in
   Term.mkVar t
 
 let declare_new_variable v constr_t =
-  let _ = Command.declare_assumption false (Decl_kinds.Local, false, Decl_kinds.Definitional) (constr_t, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, v) in
+  let _ = Command.declare_assumption false (Decl_kinds.Discharge, false, Decl_kinds.Definitional) (constr_t, Univ.ContextSet.empty) [] [] false Vernacexpr.NoInline (dummy_loc, v) in
   Term.mkVar v
 
 let extern_constr = Constrextern.extern_constr true Environ.empty_env Evd.empty
diff --git a/unit-tests/Tests_verit.v b/unit-tests/Tests_verit.v
index 2be8752..53cb9fb 100644
--- a/unit-tests/Tests_verit.v
+++ b/unit-tests/Tests_verit.v
@@ -134,8 +134,8 @@ End Checker_Let2.
 
 
 Section Sat0.
-  Parse_certif_verit t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1 "sat1.smt2" "sat1.vtlog".
-  Compute Euf_Checker.checker t_i1 t_func1 t_atom1 t_form1 root1 used_roots1 trace1.
+  Parse_certif_verit t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0 "sat0.smt2" "sat0.vtlog".
+  Compute Euf_Checker.checker t_i0 t_func0 t_atom0 t_form0 root0 used_roots0 trace0.
 End Sat0.
 
 Section Sat1.
@@ -287,7 +287,7 @@ End Let2.
 
 
 Section Theorem_Sat0.
-  Time Verit_Theorem theorem_sat1 "sat0.smt2" "sat0.vtlog".
+  Time Verit_Theorem theorem_sat0 "sat0.smt2" "sat0.vtlog".
 End Theorem_Sat0.
 
 Section Theorem_Sat1.