Adapt to coq/coq#14773 (convert_concl has a ~cast argument)

With DEFAULTcast cast:false is the previous behaviour, otherwise cast:true.

src/gappatac.c

@@ -83,7 +83,14 @@ let map_constr f t =
   EConstr.map !global_evd f t
 
 let keep a = Proofview.V82.of_tactic (Tactics.keep a)
-let convert_concl_no_check a b = Proofview.V82.of_tactic (Tactics.convert_concl ~check:false a b)
+
+#if COQVERSION >= 81500
+let convert_concl_no_check a =
+  Proofview.V82.of_tactic (Tactics.convert_concl ~cast:false ~check:false a Constr.DEFAULTcast)
+#else
+let convert_concl_no_check a =
+  Proofview.V82.of_tactic (Tactics.convert_concl ~check:false a Constr.DEFAULTcast)
+#endif
 
 #if COQVERSION < 80900
 let parse_entry e s = Pcoq.Gram.entry_parse e (Pcoq.Gram.parsable s)
@@ -553,7 +560,7 @@ let gappa_quote gl =
       (Tacticals.tclTHEN
         (generalize (List.map (fun (n, _) -> mkVar (binder_name n)) (List.rev l)))
         (keep []))
-      (convert_concl_no_check e Constr.DEFAULTcast) gl
+      (convert_concl_no_check e) gl
   with
     | NotGappa t ->
       Hashtbl.clear var_terms;