Merge branch 'master' of github.com:smtcoq/smtcoq into coq-8.10

4 files changed, 32 insertions, 4 deletions

diff --git a/src/trace/smtAtom.ml b/src/trace/smtAtom.ml
index 62cbe99..ff6db6a 100644
--- a/src/trace/smtAtom.ml
+++ b/src/trace/smtAtom.ml
@@ -1096,6 +1096,8 @@ module Atom =
       Hashtbl.find op_coq_terms
 
 
+    exception UnknownUnderForall
+
     let of_coq ?eqsym:(eqsym=false) rt ro reify known_logic env sigma c =
       let op_tbl = Lazy.force op_tbl in
       let get_cst c =
@@ -1361,10 +1363,17 @@ module Atom =
                        let i = Structures.destRel c in
                        let n, _ = Structures.destruct_rel_decl (Environ.lookup_rel i env) in
                        Some (Structures.string_of_name n)
-                     else
+                     else if Vars.closed0 c then
                        None
+                     else
+                       (* Uninterpreted expression depending on a quantified variable.
+                          We do not handle it for the moment.
+                          We leave for future work to have "dependent" constants.
+                        *)
+                       raise UnknownUnderForall
             in
-            Op.declare ro c targs tres os in
+            Op.declare ro c targs tres os
+        in
         (try
            let (i, _) = destruct "" op in
            Hashtbl.add op_coq_terms i c (* Chantal: I think we should move it to "Not_found" (otherwise it is already in the table) *)
diff --git a/src/trace/smtAtom.mli b/src/trace/smtAtom.mli
index 17a0cd0..37fcd88 100644
--- a/src/trace/smtAtom.mli
+++ b/src/trace/smtAtom.mli
@@ -140,6 +140,7 @@ module Atom :
       val print_atoms : reify_tbl -> string -> unit
 
       (** Given a coq term, build the corresponding atom *)
+      exception UnknownUnderForall
       val of_coq : ?eqsym:bool -> SmtBtype.reify_tbl -> Op.reify_tbl ->
         reify_tbl -> SmtMisc.logic -> Environ.env -> Evd.evar_map -> Structures.constr -> t
 
diff --git a/src/trace/smtCommands.ml b/src/trace/smtCommands.ml
index 5b65f5c..f626a96 100644
--- a/src/trace/smtCommands.ml
+++ b/src/trace/smtCommands.ml
@@ -689,7 +689,7 @@ let gen_rel_name =
 
 let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
   let warn () =
-    Structures.warning "Lemma" ("Discarding the following lemma (axiom form unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (Structures.extern_constr clemma))));
+    Structures.warning "Lemma" ("Discarding the following lemma (unsupported): "^(Pp.string_of_ppcmds (Ppconstr.pr_constr_expr Environ.empty_env Evd.empty (Structures.extern_constr clemma))));
     None
   in
 
@@ -714,7 +714,11 @@ let of_coq_lemma rt ro ra_quant rf_quant env sigma solver_logic clemma =
   let core_smt =
     match core_f with
       | Some core_f ->
-         Some (Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env_lemma sigma) rf_quant core_f)
+         (try
+            Some (Form.of_coq (Atom.of_coq ~eqsym:true rt ro ra_quant solver_logic env_lemma sigma) rf_quant core_f)
+          with
+            | Atom.UnknownUnderForall -> warn ()
+         )
       | None -> None
   in
   let forall_args =
diff --git a/unit-tests/Tests_verit_tactics.v b/unit-tests/Tests_verit_tactics.v
index d1c57f4..7701753 100644
--- a/unit-tests/Tests_verit_tactics.v
+++ b/unit-tests/Tests_verit_tactics.v
@@ -1249,3 +1249,17 @@ Section SearchApp.
       search x (l1 ++ l2 ++ l3) = search x (l3 ++ l2 ++ l1).
   Proof. verit. Qed.
 End SearchApp.
+
+
+Section UnknowUnderForall.
+  Variable H5 : forall H : Z, Some H = None -> False.
+  Variable H10 : @hd_error Z nil = None.
+  Variable H6 : forall H : list (list Z),
+      hd_error H = match H with
+                   | nil => None
+                   | x :: _ => Some x
+                   end.
+
+  Goal forall (l : list Z) (x : Z), hd_error l = Some x -> l <> nil.
+  Proof. verit. Qed.
+End UnknowUnderForall.